Optimization

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Semidefinite Programming 2: If Every Step Lowers the Potential φ by δ > 0, Then After k ≥ (ν√n log(1/ε) + ψ(x⁽⁰⁾, Z⁽⁰⁾))/δ Steps the Duality Gap Is at Most ε Times Its Initial ValueResearch Paper

Motivation

Semidefinite programs optimize a linear objective while requiring an affine matrix to be positive semidefinite. They include familiar linear and quadratic optimization models and arise in engineering and combinatorial optimization. Vandenberghe and Boyd's survey develops their duality theory and describes interior point methods that work with primal and dual matrices simultaneously. The question in this mission is quantitative: if a method lowers a particular potential by a fixed amount at each step, how quickly does its primal-dual objective gap shrink? Vandenberghe and Boyd, pp. 49, 76–77.

The paper uses the potential to combine two kinds of progress. One term records the size of the duality gap; another records how far the current matrices are from a central pair. Decreasing the gap alone does not ensure the matrices remain well positioned for the next step, so the potential accounts for both quantities. Theorem 5.1 turns a per-step decrease in this scalar into an explicit bound on the gap after $k$ steps. The theorem concerns any sequence meeting that decrease condition; it does not prescribe a particular search direction or step-selection algorithm. Vandenberghe and Boyd, pp. 76–77.

Setting

Fix a vector $c\in\mathbb R^m$ and symmetric real $n\times n$ matrices $F_0,F_1,\ldots,F_m$ . For $x\in\mathbb R^m$ , define the affine matrix

F(x)=F_0+\sum_{i=1}^{m}x_iF_i.

The primal problem minimizes $c^Tx$ subject to $F(x)\succeq0$ . A dual-feasible matrix $Z$ satisfies $Z\succeq0$ and $\operatorname{Tr}(F_iZ)=c_i$ for every $i=1,\ldots,m$ . Here $\succeq0$ means positive semidefinite; $\succ0$ means positive definite. The pair $(x,Z)$ is strictly feasible if both $F(x)\succ0$ and $Z\succ0$ , with the dual equations still satisfied. Section 4 also assumes that $F_1,\ldots,F_m$ are linearly independent. Vandenberghe and Boyd, pp. 49, 63, 70.

For a feasible pair, the duality gap is the difference between the primal objective $c^Tx$ and the dual objective $-\operatorname{Tr}(F_0Z)$ . Equation (32) identifies it as

\eta=c^Tx+\operatorname{Tr}(F_0Z)=\operatorname{Tr}(F(x)Z).

For a strictly feasible pair, define the deviation from centrality and the potential by

\psi(x,Z)=-\log\det(F(x)Z)+n\log\eta-n\log n,

\varphi(x,Z)=\nu\sqrt n\,\log\eta+\psi(x,Z),\qquad \nu\ge1.

The logarithm is natural. The matrix size $n$ determines the $\sqrt n$ factor; it is distinct from the number $m$ of decision variables. These are the explicit formulas on p. 76, where the paper also expresses $\psi$ through a central pair. Vandenberghe and Boyd, pp. 64, 75–76.

Formalization targets

The first milestones establish the gap identity, the expanded determinant formula for $\varphi$ , and nonnegativity of $\psi$ with its stated equality condition. The final milestone bounds the gap by the potential:

\eta\le\exp\!\left(\frac{\varphi(x,Z)}{\nu\sqrt n}\right).

For the goal, let $(x^{(j)},Z^{(j)})$ , $j=0,\ldots,k$ , be strictly feasible pairs and suppose a fixed $\delta>0$ gives the decrease stated in equation (56) at every step $j<k$ :

\varphi(x^{(j+1)},Z^{(j+1)})\le\varphi(x^{(j)},Z^{(j)})-\delta.

The goal theorem, Theorem 5.1, says that for $0<\varepsilon<1$ and

k\ge\frac{\nu\sqrt n\log(1/\varepsilon)+\psi(x^{(0)},Z^{(0)})}{\delta},

one has the boundary-correct gap estimate

\operatorname{Tr}(F(x^{(k)})Z^{(k)})\le\varepsilon\operatorname{Tr}(F(x^{(0)})Z^{(0)}).

The paper prints a strict inequality in the last display. Its stated non-strict threshold permits equality, as explained under Formalization scope. Vandenberghe and Boyd, p. 77, (56) and Theorem 5.1.

Significance

The theorem converts a local numerical guarantee into a global bound on an optimization certificate. Because the gap is the difference between primal and dual objectives, shrinking it gives a quantitative measure of progress toward optimality for every strictly feasible iterate. The expression records the dependence on matrix size, desired relative gap, starting deviation, and guaranteed potential decrease. It leaves the mechanism that achieves the decrease open, so different potential reduction methods can use the same conclusion. Vandenberghe and Boyd, pp. 64, 76–77.

The target here is a machine-checked statement and proof of this known 1996 result, together with its four supporting facts. The draft declarations compile as statements; their proofs remain open. A complete development would make the determinant, trace, positive-definiteness, and sequence reasoning reusable for other matrix optimization arguments. It would also record the boundary correction precisely rather than carrying forward a strict sign that fails at equality.

Difficulty

The substantive matrix claim is $\psi(x,Z)\ge0$ . The product $F(x)Z$ need not be symmetric, even though both factors are positive definite, so directly applying a result about symmetric matrix eigenvalues to the product is not automatic. The nonnegativity and its equality case must respect the positivity and determinant conventions used by the explicit formula. The later exponential bound and iteration statement depend on those facts and on keeping each logarithm in its positive domain. Vandenberghe and Boyd, p. 76.

Formalization scope

Lean uses Fin m for the $m$ variable matrices, indexed from zero, with $F_0$ as a separate argument; Fin n indexes matrix rows and columns. Matrix.IsHermitian represents real symmetry. Matrix.PosSemidef and Matrix.PosDef represent the paper's matrix inequalities $\succeq0$ and $\succ0$ , including symmetry. The matrix size satisfies $n\ge1$ . Traces, determinants, natural logarithms, and $\sqrt n$ are the corresponding Mathlib operations. All statements involving $\psi$ or $\varphi$ require strict feasibility, so the real logarithm's default value on nonpositive inputs cannot decide a theorem. The paper's linearly independent $F_1,\ldots,F_m$ are an explicit hypothesis on the Section 4 and 5 statements. Vandenberghe and Boyd, pp. 49, 70, 76–77.

The definition of $\psi$ uses the explicit second formula on p. 76. The central pair in the preceding formula is not represented; its existence is introduced on p. 75 without a proof there. The p. 76 prose describes $\psi\ge0$ for feasible pairs, but its finite real logarithmic formula and the potential reduction iterates use strictly feasible pairs. The milestone states that domain explicitly. In Theorem 5.1 strict feasibility is assumed for the iterates $j=0,\ldots,k$ and equation (56) for the steps $j<k$ only, so the statement covers a method that stops after $k$ steps. The fixed $\delta$ is positive, and $\nu\ge1$ and $0<\varepsilon<1$ are explicit.

The paper's strict conclusion is false at its own inclusive threshold. Take $m=n=1$ , $F_0=0$ , $F_1=c=Z^{(j)}=1$ , $x^{(j)}=e^{-j}$ , $\nu=\delta=1$ , and $\varepsilon=e^{-1}$ . Then $\psi=0$ , each decrease is exactly one, and at $k=1$ the gap equals $\varepsilon$ times its initial value. The goal therefore uses $\le$ , the strongest statement valid at the printed threshold. This correction is recorded in the theorem's description and moderation notes. Vandenberghe and Boyd, p. 77, Theorem 5.1.

A complete proof needs Mathlib's matrix order, determinant and trace identities, logarithm and exponential facts, and an arithmetic-geometric mean statement for positive eigenvalues. Matrix lemmas and the deviation inequality are welcome contributions alongside the final sequence bound. The definitions preserve the paper's full potential and feasible domain; replacing $\psi$ by zero or dropping the $\sqrt n$ factor would change the target.

Selected references

Lieven Vandenberghe and Stephen Boyd, Semidefinite Programming, SIAM Review 38(1), 49–95, 1996. DOI: 10.1137/1038003.

9 thms3 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Monotone Comparative Statics II: f Is Quasisupermodular If and Only If a Strictly Increasing Transformation Makes It Supermodular on Every Sublattice {x₁, x₂, x₁ ∨ x₂, x₁ ∧ x₂}Research Paper

Motivation

Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.

Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). Examples are $\mathbb{R}^n$ and products of finite chains, ordered componentwise.

A function $f : X \to \mathbb{R}$ is supermodular on a set $S \subseteq X$ if

f(x) + f(y) \le f(x \vee y) + f(x \wedge y) \qquad \text{for all } x, y \in S.

It is quasisupermodular (p. 162) if for all $x, y \in X$

$f(x) \ge f(x \wedge y)$ implies $f(x \vee y) \ge f(y)$ , and
$f(x) > f(x \wedge y)$ implies $f(x \vee y) > f(y)$ .

A function $h : \mathbb{R} \to \mathbb{R}$ is strictly increasing if $r < s$ implies $h(r) < h(s)$ . A function $f$ is supermodularizable if $h \circ f$ is supermodular on $X$ for some strictly increasing $h$ .

For $x_1, x_2 \in X$ the set $\{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}$ is closed under $\vee$ and $\wedge$ ; it is the sublattice generated by $x_1$ and $x_2$ and has at most four points.

Quasisupermodularity depends only on the order of the values of $f$ , so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.

Formalization targets

Goal: Theorem 8 (p. 165)

$f : X \to \mathbb{R}$ is quasisupermodular if and only if there is $g : \mathbb{R} \times X \times X \to \mathbb{R}$ such that (i) $r \mapsto g(r, x_1, x_2)$ is strictly increasing for every $(x_1, x_2) \in X^2$ , and (ii) for every $x_1, x_2 \in X$ ,

x \mapsto g(f(x), x_1, x_2) \ \text{ is supermodular on } \{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}.

Milestones

Invariance (p. 164): if $f$ is quasisupermodular and $g$ strictly increasing, $g \circ f$ is quasisupermodular.
Supermodularizable implies quasisupermodular (pp. 164–165): if $h$ is strictly increasing and $h \circ f$ is supermodular on $X$ , then $f$ is quasisupermodular.
Lemma (p. 165): if $f$ is quasisupermodular on $L = \{x, x', x \vee x', x \wedge x'\}$ , then $h \circ f$ is supermodular on $L$ for some strictly increasing $h : \mathbb{R} \to \mathbb{R}$ .
Example 1 (p. 165): the function on $\{0,1\} \times \{0,1,2,3\}$ with rows $(1,2,2,1)$ and $(3,4,5,3)$ is quasisupermodular but not supermodularizable.

The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on $(x_1, x_2)$ .

Significance

Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.

On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of $\mathbb{R}$ that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.

Difficulty

The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values $a, b, c, d$ of $f$ at $x, x \vee x', x \wedge x', x'$ need not satisfy $a + d \le b + c$ , and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing $h$ of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which $x$ and $x'$ are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair $(x, x')$ .

Formalization scope

Lattices are Mathlib's Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.
Quasisupermodularity is a draft definition QuasiSupermodularOn g S, relativized to a set $S$ ; the paper's notion on $X$ is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of $S$ .
Supermodularity is the published definition Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.
"Strictly increasing" is StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.
The transformation $g : \mathbb{R} \times X \times X \to \mathbb{R}$ of Theorem 8 is curried, g : ℝ → X → X → ℝ; it may depend on $(x_1, x_2)$ but not on $x$ . Transformations are defined on all of $\mathbb{R}$ , as printed, not only on the values of $f$ .
The Lemma's four-point lattice is formalized as the subset $\{x, x', x \vee x', x \wedge x'\}$ of an ambient lattice, with both notions relativized to it; the subset is closed under join and meet, so this is the page's statement, including the degenerate cases.
Example 1's domain is Fin 2 × Fin 4 with the product order.

Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps $\mathbb{R} \to \mathbb{R}$ with prescribed values on finitely many points.

Selected references

P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
M. Li Calzi, Generalized Symmetric Supermodular Functions, Working Paper, Stanford University, 1990 (listed so in the paper's references; the text on p. 165 cites it as Li Calzi (1991)).

8 thms3 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Learning Models with Uniform Performance via Distributionally Robust Optimization 2: A Minimax Lower Bound of Order n^(−1/2) ∨ n^(−1/k*) for Estimating the Cressie–Read Robust Risk (Theorem 3)Research Paper

Motivation

Distributionally robust optimization replaces the expected loss $\mathbb E_{P_0}[\ell(\theta; X)]$ of a statistical model by its worst case over all distributions $Q$ close to the data distribution $P_0$ . When closeness is measured by an $f$ -divergence ball $\{Q : D_f(Q\|P_0) \le \rho\}$ of fixed radius $\rho > 0$ , the robust risk upper-bounds the risk of every subpopulation of $P_0$ that has sufficiently large probability, so a model with small robust risk performs uniformly well across latent subgroups. This is the program of J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization (arXiv:1810.08750; Ann. Statist. 49 (2021), doi:10.1214/20-AOS2004).

The robust risk is itself a statistical functional. It is estimated by plugging in the empirical distribution, and the paper shows (its Theorem 2) that for the Cressie–Read family of divergences with parameter $k$ the plug-in estimate concentrates at rate $n^{-1/(k_* \vee 2)}$ , with $k_* = k/(k-1)$ . For small $k$ (heavy protection against distribution shift) $k_*$ is large and this rate is far slower than the parametric $n^{-1/2}$ . This mission formalizes the paper's answer to whether the slow rate is an artefact of the plug-in estimator or intrinsic: its Theorem 3, a minimax lower bound valid for every estimator.

Setting

Fix $k \in (1,\infty)$ and write $k_* = k/(k-1)$ . The Cressie–Read function is

f_k(t) = \frac{t^k - kt + k - 1}{k(k-1)} \quad (t \ge 0), \qquad f_k(t) = +\infty \quad (t < 0).

For a probability measure $P$ , a real random variable $Z$ and a radius $\rho > 0$ , the robust risk is

\mathcal R_k(Z) = \sup\Bigl\{ \mathbb E_P[LZ] : L \ge 0,\ \mathbb E_P[L] = 1,\ \mathbb E_P[f_k(L)] \le \rho \Bigr\},

the supremum of $\mathbb E_Q[Z]$ over distributions $Q \ll P$ with likelihood ratio $L = dQ/dP$ and Cressie–Read divergence $D_{f_k}(Q\|P) = \mathbb E_P[f_k(L)]$ at most $\rho$ .

Write

c_k(\rho) = (1 + k(k-1)\rho)^{1/k}, \qquad p_k = (1 + k(k-1)\rho)^{-1/(k-1)}, \qquad \beta_k = \frac{k(k-1)\rho}{2(1+k(k-1)\rho)} .

Fix $M > 0$ and let $\mathcal P$ be the set of all distributions on the two points $\{0, M\}$ ; each is determined by its mass $p \in [0,1]$ at $M$ . An estimator is any function $\widehat R : \{0, M\}^n \to \mathbb R$ of a sample $Z_1^n = (Z_1, \dots, Z_n)$ drawn i.i.d. from $P_0 \in \mathcal P$ . The minimax risk of estimating the robust risk is

\mathfrak M_n(\mathcal P, f_k) = \inf_{\widehat R}\ \sup_{P_0 \in \mathcal P}\ \mathbb E_{P_0^n}\bigl|\widehat R(Z_1^n) - \mathcal R_k(Z)\bigr|, \qquad Z \sim P_0. \qquad (16)

The total variation distance between two product laws $P^n, P'^n$ on the finite set $\{0,M\}^n$ is $\|P^n - P'^n\|_{\mathrm{TV}} = \tfrac12\sum_z |P^n\{z\} - P'^n\{z\}|$ , and $D_{\mathrm{kl}}$ denotes the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 3

For every $n \ge 1$ ,

\mathfrak M_n(\mathcal P, f_k) \ge M \max\Biggl\{ \frac{1}{8 k_* p_k}\Bigl( \sqrt{\frac{p_k(1-p_k)}{16 n}} \wedge \tfrac12(1-p_k) \wedge p_k \Bigr),\ \ \frac18 \beta_k^{1/k} c_k(\rho) \Bigl( \frac{1}{4n} \wedge p_k \wedge \bigl(1 - (1-\beta_k)^{1-k_*} p_k\bigr) \Bigr)^{1/k_*} \Biggr\}.

The first branch is of order $n^{-1/2}$ , the second of order $n^{-1/k_*}$ . The page prints $8n$ in the first branch; the target uses $16n$ (see Formalization scope).

Milestones

Lemma 12 (three claims): for $Z$ equal to $z_0 \le z_1$ with probabilities $1-p$ , $p$ : if $p \ge p_k$ then $\mathcal R_k(Z) = z_1$ ; if $p \le p_k$ then $\mathcal R_k(Z) \le c_k p^{1/k_*} z_1 + (1 - c_k p^{1/k_*}) z_0$ ; and if $p \le p_k \wedge (1 - (1-\beta)^{1-k_*} p_k)$ for some $\beta \in (0,1)$ then $\mathcal R_k(Z) \ge \beta^{1/k} c_k p^{1/k_*} z_1 + (1 - \beta^{1/k} c_k p^{1/k_*}) z_0$ .
The primal two-point formula (p. 47): for $p \in (0,1)$ ,

\mathcal R_k(Z) = z_0 + (z_1 - z_0)\sup\{q \in [0,1] : (1-p)^{1-k}(1-q)^k + p^{1-k}q^k \le c_k^k\}.

Le Cam's reduction (37): if $|\mathcal R_k(P_0) - \mathcal R_k(P_1)| \ge 2\delta > 0$ then $\mathfrak M_n \ge \frac\delta2(1 - \|P_0^n - P_1^n\|_{\mathrm{TV}})$ .
The Taylor display $c_k(p_k - \delta)^{1/k_*} \le 1 - \frac{1}{k_*}c_k^{k_*}\delta$ for $0 < \delta \le p_k$ .
The KL display $D_{\mathrm{kl}}(P_2\|P_1) \le 8\delta^2/(p_k(1-p_k))$ for the laws with masses $p_k \mp \delta$ at $M$ .
Pinsker for products $\|P_1^n - P_2^n\|_{\mathrm{TV}}^2 \le \frac n2 D_{\mathrm{kl}}(P_2\|P_1)$ .
The second-branch KL display $-\log(1-\delta) \le \delta/(1-\delta) \le 2\delta$ for $\delta \le \frac12$ .

Significance

Theorem 3 shows that the rate $n^{-1/(k_* \vee 2)}$ of the paper's concentration bound for the plug-in robust risk cannot be improved by any estimator, even when the data take only two values. For $k < 2$ the robust risk is therefore intrinsically harder to estimate than a mean: its value depends on how much mass $P_0$ puts on rare large values, and rare events are observed rarely. The same phenomenon drives the paper's lower bounds for minimizing the robust risk (its Section 5.2), which are not part of this mission.

The result is proved in the paper; no machine-checked version of it or of Lemma 12 is known. Formalizing it produces a verified two-point analysis of the Cressie–Read robust risk (Lemma 12 and its primal formula), which is reusable for any lower bound or worked example involving $f$ -divergence balls, and a verified finite-sample Le Cam two-point bound for estimating a functional of a distribution on two points. It also corrects a constant in the first branch of the printed statement.

Difficulty

The lower bound needs two distributions on $\{0,M\}$ that are statistically close yet have well-separated robust risks. Both requirements must be quantitative and must hold simultaneously at the stated constants. The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so the separation needs exact control of that supremum for two-point laws: an exact value above the threshold $p_k$ , and matching upper and lower bounds below it. For mass near $p_k$ the separation is linear in $\delta$ , while for small mass it is of order $\delta^{1/k_*}$ , which is where the slow rate comes from. Closeness requires the KL divergence of each pair to be at most $1/(2n)$ , and the two branches need different perturbations. A naive bound on the robust risk by $\max(z_0, z_1)$ or by the mean gives no separation at all.

Formalization scope

The Lean development lives in the namespace UniformDRO.LowerBound. Its conventions are:

$k > 1$ , $\rho > 0$ , $M > 0$ (all on the page); $n \ge 1$ in the goal (implicit on the page, since the bound contains $1/n$ ).
The robust risk is the real supremum in the likelihood-ratio form above, with the divergence constraint written as a lower Lebesgue integral of $f_k(L) \ge 0$ . Absolute continuity $Q \ll P$ is built in. For a two-point law the feasible values lie between the two points, so the supremum is genuine.
Laws on $\{0,M\}$ are $(1-p)\delta_0 + p\,\delta_M$ , $p \in [0,1]$ . Expectations under $P_0^n$ are finite sums over $\{0,M\}^n$ . The minimax risk takes values in $[0,\infty]$ , with the infimum over all real functions of the sample taken outside the supremum over $p$ . For these laws it agrees with the platform's general HighDimStat.Minimax.minimaxRisk.
$D_{\mathrm{kl}}$ between two-point laws is the platform's BanditAlgorithm.bernoulliRelativeEntropy, always evaluated with a second argument in $(0,1)$ , where it is the true divergence.
Real powers are Real.rpow. The primal formula is stated for $p \in (0,1)$ , where its negative powers are finite.
Correction of the print. In Theorem 3 the page has $\sqrt{p_k(1-p_k)/(8n)}$ . The paper's argument with that choice gives $D_{\mathrm{kl}} \le 1/n$ and, by Pinsker, total variation at most $1/\sqrt2$ , which does not yield the printed constant $1/(8k_*p_k)$ . The target uses $16n$ , for which the same argument gives total variation at most $\tfrac12$ and exactly the printed constant. The second branch is as printed. The milestone quotes keep the page's text.

The goal is the lower bound on the minimax risk (16) over all estimators and all laws on $\{0,M\}$ . It does not mention the two hypotheses, $\delta$ , total variation or KL divergence, so it cannot be satisfied by a statement about a particular pair of laws or a particular estimator.

Contributions are welcome at every level: proofs of Lemma 12 through the primal formula or through the dual representation of the robust risk, a general finite-space Le Cam lemma, and tensorization of KL and Pinsker for finite products, which are reusable beyond this mission.

Selected references

J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization, Ann. Statist. 49(3), 2021; arXiv:1810.08750v6. https://arxiv.org/abs/1810.08750, https://doi.org/10.1214/20-AOS2004
L. Le Cam, Asymptotic Methods in Statistical Decision Theory, Springer, 1986. https://doi.org/10.1007/978-1-4612-4946-7
B. Yu, Assouad, Fano, and Le Cam, in Festschrift for Lucien Le Cam, Springer, 1997, 423–435. https://doi.org/10.1007/978-1-4612-1880-7_29
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
N. Cressie and T. R. C. Read, Multinomial goodness-of-fit tests, J. R. Stat. Soc. B 46(3), 1984, 440–464. https://doi.org/10.1111/j.2517-6161.1984.tb01318.x

13 thms3 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Bounded Rationality in Newsvendor Models V: If σ_T ≤ Σσ_i and σ_T ≥ σ_i, Pooling Strictly Lowers the Expected Cost of Logit Newsvendors with Normal DemandsResearch Paper

Motivation

Inventory pooling lets several locations serve their combined demand from one stock of goods. Classical newsvendor analysis predicts lower optimal cost when pooling reduces demand variation, but the reduction can vanish when demands are perfectly correlated. Xuanming Su asks whether that conclusion survives when managers make noisy stocking decisions rather than always choose the optimum. In the published 2008 article, Bounded Rationality in Newsvendor Models, the decision noise follows a continuous logit model, in which better quantities are chosen more often. Proposition 7 gives conditions under which pooling strictly lowers expected cost, including a case where classical pooling has no cost gain. Su, 2008

The question matters for multilocation inventory systems because an order quantity is a decision as well as a response to demand. Pooling changes both the distribution of demand faced by the system and the number of independently chosen orders. A comparison based only on optimal costs leaves the second change out. This mission isolates the paper's mathematical claim about the combined effect of demand and decision variation. Su, 2008, §9

Setting

There are $n$ locations. Demand at location $i$ is normally distributed with mean $\mu_i$ and standard deviation $\sigma_i$ . The total demand has normal law with mean $\mu_T=\sum_i\mu_i$ and standard deviation $\sigma_T$ . An order of $x$ against a realized demand $D$ incurs holding cost $h(x-D)^+$ for unsold units and backlog cost $b(D-x)^+$ for unmet demand. Its expected cost is $\gamma(x)$ . The decentralized system incurs one such cost at each location; the pooled system orders once for total demand. The published InventoryControl_newsboy definition supplies this Gaussian expected cost, with the same orientation of holding and backlog penalties as Su's equations (29) and (31). Su, 2008, p. 584

For an expected profit function $\pi$ on a decision set $S$ , the logit choice density is proportional to $e^{\pi(x)/\beta}$ on $S$ , where $\beta>0$ is a common bounded-rationality parameter. Larger $\beta$ spreads choices more widely; smaller positive $\beta$ concentrates them near high-profit choices. For normal demand, the decision domain is all of $\mathbb R$ . With $p=h+b$ and $c=h$ , expected profit differs from minus expected cost by a constant independent of the order. The same logit law is therefore obtained from utility $-\gamma(x)$ . The random behavioral order is denoted $X_i^b$ at location $i$ and $X_T^b$ for the pool. Su, 2008, pp. 571–572, 584

Formalization targets

Strict pooling reduction

The goal is Proposition 7. Under positive holding and backlog costs, one common positive $\beta$ , at least two locations, positive individual standard deviations, and

\sigma_T\leq\sum_{i=1}^{n}\sigma_i, \qquad \sigma_T\geq\sigma_i\quad\text{for every }i,

the claim is

\mathbb E\bigl[\gamma_T(X_T^b)\bigr] <\sum_{i=1}^{n}\mathbb E\bigl[\gamma_i(X_i^b)\bigr].

The first standard-deviation inequality is automatic for the sum of jointly normal demands. The second excludes a total demand whose standard deviation is smaller than an individual location's. The result still includes perfect positive correlation, where the first inequality is an equality. Su, 2008, Proposition 7, p. 585

Supporting statements

Five milestones record the source's route to that comparison: invariance of the choice distribution under an order-preserving affine change of quantity (Lemma 1), invariance under an additive shift in utility (Lemma 2), standardization of the Gaussian newsvendor objective (equation (63)), the optimum of the canonical standard-normal newsvendor and the nonpositivity of its profit, and the comparison of its expected values at different positive scales. The milestone text preserves the wording of the printed article; the precise Lean conditions and corrections are stated with the items. Su, 2008, pp. 572, 587–588

Significance

The strict inequality separates two mechanisms of pooling. Demand aggregation can reduce variability, while a single pooled order also avoids accumulating the costs of several noisy decisions. Proposition 7 shows that the latter mechanism can make the cost reduction strict even when perfect correlation removes the usual variance benefit. It provides a condition that can be checked from individual and total standard deviations, rather than requiring an explicit covariance matrix in the final comparison. Su, 2008, pp. 584–585

The result is proved in the paper; the remaining task is a machine-checked formalization of its definitions and argument. The Gaussian expected-cost object is already published on Prove2Me, while the continuous logit law and this behavioral pooling theorem are new to this mission. The invariance statements and canonical profit comparison are reusable wherever a continuous logit rule acts on a transformed one-dimensional objective.

Difficulty

The usual pooling comparison evaluates cost at an optimal order. Here each system draws its order from a different continuous probability law, and the cost to compare is averaged over those choices. Comparing $\sigma_T$ with $\sum_i\sigma_i$ alone does not compare the logit distributions; in particular, it gives equality under perfect positive correlation while the target is strict. A formal development must also show that the normalizing integrals and the resulting cost expectations are genuine finite integrals for every set of parameters covered by the theorem.

Formalization scope

The Lean model uses Mathlib's real Gaussian law with variance $\sigma^2$ and the published InventoryControl_newsboy.newsboyCost for equations (29) and (31). It records the choice density, CDF, expectation, canonical profit, and behavioral expected cost as separate definitions. The behavioral density uses $e^{-\gamma/\beta}$ on $\mathbb R$ ; the utility shift from profit is covered by Lemma 2. The theorem specifies normal marginals and a normal total with mean $\sum_i\mu_i$ and standard deviation $\sigma_T$ . Every jointly normal demand vector in the paper yields these laws, and the final comparison uses no further feature of its joint distribution.

The conditions $h>0$ , $b>0$ , and $\beta>0$ are standing readings needed for the continuous choice law on the unbounded domain. Proposition 7 additionally states $n\geq2$ and $\sigma_i>0$ : for one location the alleged strict comparison becomes equality, while zero variance makes the paper's continuous density on a point support undefined. Lemma 1 requires positive affine scale because a negative scale reverses CDF order, and its two invariance lemmas require a finite positive normalizer. Equation (66) is read with $\min(Z,z)$ , as dictated by the surrounding formulas; the printed display drops the word “min.” These corrections and the cost-based choice convention are recorded item by item in the moderation notes.

No optimizer is supplied as a free variable, and no zero normalizer is allowed to turn a logit expectation into a trivial zero. Useful solver contributions include proofs that the cost-based logit normalizer and expected cost are integrable, Gaussian change-of-variables lemmas, and the strict scale comparison. These analytic facts can serve other continuous-choice models.

Selected references

Xuanming Su, Bounded Rationality in Newsvendor Models, Manufacturing & Service Operations Management 10(4):566–589, 2008. DOI: 10.1287/msom.1070.0200.

9 thms3 active usersReviewed

Completed

Convex Optimization·Captain: mikedeng1

Primal-dual subgradient methods for convex problems 1: Dual Averaging Keeps the Gap Below β_{k+1}D + (1/2σ)Σλᵢ²‖gᵢ‖²_*/βᵢ and Its Iterates BoundedResearch Paper

Motivation

Subgradient methods are the basic tool for minimizing a nonsmooth convex function when only a black-box oracle returning one subgradient per query is available. In the classical method the new subgradient enters the iterate with a weight that decreases over time, so information collected late is counted less than information collected early, and the method has no natural certificate of its own accuracy.

Yu. Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009) 221–259; first circulated as a CORE discussion paper, March 2002, revised September 2005) introduces Dual Averaging (DA): the method accumulates all past subgradients with nondecreasing weights in the dual space and maps the aggregate back to the feasible set through a strongly convex prox-function. One analysis, Theorem 1 of the paper, gives at once an upper bound on a primal-dual gap, a bound on the iterates that holds even on unbounded feasible sets, and a bound on the averaged subgradients. From it the paper derives rates for minimization over simple sets, problems with functional constraints, saddle points, variational inequalities, and stochastic optimization. Dual Averaging later became a standard method in online learning and regularized stochastic optimization (e.g. L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, JMLR 11 (2010)).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ , and $E^*$ its dual. The value of $s \in E^*$ at $x \in E$ is $\langle s, x\rangle$ , and the dual norm is $\|s\|_* = \max\{\langle s, x\rangle : \|x\| \le 1\}$ . Balls are $B_r(x) = \{y : \|y - x\| \le r\}$ .

Let $Q \subseteq E$ be closed and convex. A prox-function of $Q$ is a function $d$ , continuous on $Q$ , that is strongly convex on $Q$ with convexity parameter $\sigma > 0$ :

d(\alpha x + (1-\alpha)y) \le \alpha d(x) + (1-\alpha) d(y) - \tfrac12\sigma\alpha(1-\alpha)\|x - y\|^2, \qquad x, y \in Q,\ \alpha\in[0,1].

The prox-center $x_0 \in Q$ minimizes $d$ on $Q$ , and $d(x_0) = 0$ . Two examples: the Euclidean norm with $d(x) = \frac12\|x - x_0\|_2^2$ , and the $\ell_1$ norm on the simplex with the entropy $d(x) = \ln n + \sum_i x^{(i)}\ln x^{(i)}$ .

For $D \ge 0$ and $\beta > 0$ set $F_D = \{x \in Q : d(x) \le D\}$ and

\xi_D(s) = \max_{x\in F_D}\langle s, x - x_0\rangle, \qquad V_\beta(s) = \max_{x\in Q}\{\langle s, x - x_0\rangle - \beta d(x)\},

and let $\pi_\beta(s) = \arg\min_{x\in Q}\{-\langle s, x\rangle + \beta d(x)\}$ .

Given sequences $x_i \in E$ , $g_i \in E^*$ , $\lambda_i$ , write $S_k = \sum_{i=0}^k \lambda_i$ , $s_{k+1} = \sum_{i=0}^k \lambda_i g_i$ ( $s_0 = 0$ ), $\hat s_{k+1} = s_{k+1}/S_k$ , the gap function

\delta_k(D) = \max_{x\in F_D}\sum_{i=0}^k \lambda_i\langle g_i, x_i - x\rangle,

and the upper gap function $\Delta_k(\beta, D) = \beta D + \sum_{i=0}^k \lambda_i\langle g_i, x_i - x_0\rangle + V_\beta(-s_{k+1})$ .

The DA-scheme (2.14) starts at $x_0$ with $s_0 = 0$ and $\beta_0 > 0$ ; at step $k \ge 0$ it receives $g_k$ (the oracle answer at $x_k$ ), chooses $\lambda_k > 0$ and $\beta_{k+1} \ge \beta_k$ , and sets

s_{k+1} = s_k + \lambda_k g_k, \qquad x_{k+1} = \pi_{\beta_{k+1}}(-s_{k+1}).

A point $x^* \in Q$ is a solution in the sense (2.8) if $\langle g_i, x_i - x^*\rangle \ge 0$ for all $i$ .

Formalization targets

Goal: Theorem 1 (p. 9)

For every run of the DA-scheme, every $k \ge 0$ and every $D \ge 0$ ,

\delta_k(D) \le \Delta_k(\beta_{k+1}, D) \le \beta_{k+1} D + \frac{1}{2\sigma}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2;

if $x^*$ is a solution in the sense (2.8), then

\tfrac12\sigma\|x_{k+1} - x^*\|^2 \le d(x^*) + \frac{1}{2\sigma\beta_{k+1}}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2;

and if moreover $B_r(x^*) \subseteq F_D$ for some $r, D > 0$ , then

\|\hat s_{k+1}\|_* \le \frac{1}{r S_k}\Big[\beta_{k+1}D + \frac{1}{2\sigma}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2\Big].

The theorem leaves the step sizes $\lambda_k$ and the parameters $\beta_k$ free; every rate in the paper is obtained by choosing them.

Milestones

In the order the proof uses them: Lemma 6 (unique minimizer of a strongly convex function, quadratic growth (9.5), p. 36); Lemma 1 (convexity, differentiability, $\nabla V_\beta(s) = \pi_\beta(s) - x_0$ and its $1/(\beta\sigma)$ -Lipschitz continuity, p. 7); (2.5) $V_\beta(s+\delta) \le V_\beta(s) + \langle\delta, \nabla V_\beta(s)\rangle + \frac{1}{2\sigma\beta}\|\delta\|_*^2$ ; (2.6) $V_\beta(\delta) \le \frac{1}{2\sigma\beta}\|\delta\|_*^2$ ; (2.2) monotonicity of $V_\beta$ in $\beta$ ; Lemma 2 $\xi_D(s) \le \beta D + V_\beta(s)$ (p. 8); (2.11) the representation $\delta_k(D) = \sum_i\lambda_i\langle g_i, x_i - x_0\rangle + \xi_D(-s_{k+1})$ ; (2.13) $\delta_k(D) \le \Delta_k(\beta, D)$ ; and (2.18), the telescoped estimate along the scheme (p. 10).

Significance

Theorem 1 is the single estimate behind the whole paper. With $\beta_k$ growing like $\sqrt k$ it gives the $O(1/\sqrt k)$ rate of Dual Averaging for nonsmooth convex minimization with simple or weighted averages (Theorems 2 and 3), and through the gap $\delta_k(D)$ it gives primal-dual certificates for saddle-point problems and variational inequalities (§§3–5) and the stochastic version (§6, the companion mission). Part 2 is the reason the method can run on unbounded feasible sets: the iterates stay in a ball around any solution. Part 3 bounds the averaged subgradients, which yields approximate dual solutions.

The result is proved in the paper. As far as a search of Mathlib and the Prove2Me catalog shows (October 2026), none of its statements is machine-checked: Mathlib has strong convexity (StrongConvexOn) and Fréchet derivatives, but no prox-functions in an arbitrary norm, no Danskin-type differentiability of a maximum, and no analysis of Dual Averaging. A formalization produces these as reusable pieces: Lemma 6 in an arbitrary finite-dimensional norm, the smoothness of $V_\beta$ (a form of the duality between strong convexity and Lipschitz gradients of the conjugate), and the definitions of the scheme and its gap functions, on which the paper's §§3–6 can then be built.

Difficulty

The bookkeeping of the proof is short; the analytic content sits in Lemma 1 and Lemma 6. Lemma 1 asserts differentiability of a function defined as a maximum over a possibly unbounded set, in an arbitrary norm, where the gradient lives in $E^{**}$ and no inner product is available to identify it with a vector. The prox-function is only continuous and strongly convex, never assumed differentiable (footnote 2, p. 5), so first-order optimality conditions for $\pi_\beta$ are not available. Lemma 6's existence claim needs boundedness of the level sets of $d$ in finite dimension; the printed argument ends with "this contradicts continuity of $d$ ", which does not by itself close the argument, so a complete proof has to supply the missing step. Finally, (2.18) pairs a sum from $i = 0$ with a sum from $i = 1$ and depends on $x_0$ being the prox-center, so an off-by-one in the indices of the scheme changes the statement.

Formalization scope

$E$ is a finite-dimensional real normed space with an arbitrary norm; $E^*$ is StrongDual ℝ E with the operator norm, which is $\|\cdot\|_*$ , and $\langle s, x\rangle$ is s x. No inner product is used, so the $\ell_1$ /entropy example remains an instance. The prox-function is a real function on $E$ of which only its values on $Q$ are used, strongly convex in Mathlib's sense StrongConvexOn Q σ d (exactly (1.8)), with $\sigma > 0$ (the paper's " $\sigma \ge 0$ " at (1.8) is corrected by its Definition 1). The maxima $\xi_D$ , $V_\beta$ , $\delta_k$ are real suprema, finite for $D \ge 0$ , $\beta > 0$ ; every statement assumes these ranges, including Lemma 2 and (2.13), where the page writes $\beta \ge 0$ but $V_0$ is not defined. The argmin map $\pi$ is a hypothesis on a given map, not a construction, and the run of (2.14) starts at the prox-center and takes the oracle answers $g_k$ as free data. Indices start at $0$ . Pages and equation numbers are those of the CORE discussion-paper version (September 2005) used as source, not the journal's pp. 221–259.

A trivializing formalization is ruled out: the run must set $x_{k+1}$ to the argmin point $\pi_{\beta_{k+1}}(-s_{k+1})$ and $\pi$ must carry its argmin property, without which the statements would be false, and the setting is satisfiable (E = ℝ, $Q = ℝ$ , $d(x) = x^2/2$ , $\sigma = 1$ , $\pi_\beta(s) = s/\beta$ ), so the theorem is not vacuous.

Needed infrastructure: Lemma 6 in an arbitrary norm; a Danskin-type differentiability lemma for $V_\beta$ ; Lipschitz continuity of the argmin map; suprema manipulations for $\xi_D$ , $V_\beta$ , $\delta_k$ under boundedness. Contributions of any of the milestones, of general lemmas on strongly convex functions in normed spaces, and of the remaining parts of Theorem 1 are welcome.

Selected references

Yu. Nesterov, Primal-dual subgradient methods for convex problems, Math. Program. 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, J. Mach. Learn. Res. 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
Yu. Nesterov, Smooth minimization of non-smooth functions, Math. Program. 103 (2005) 127–152. https://doi.org/10.1007/s10107-004-0552-5

12 thms3 active usersReviewed

Completed

Complexity Theory Linear Optimization Operations Research·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 2: The Adaptive-Step Algorithm in N∞(β) or N∞⁻(β) with γ ≤ 2(1 − β) Attains Precision t in O(nt) IterationsResearch Paper

Why wide neighbourhoods

Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products $x_js_j$ are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood $\{x_js_j \ge \tfrac12\,x^Ts/n\}$ and attained precision $t$ in $O(nt)$ iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood $\mathcal N_2(\beta)$ and improved the bound to $O(\sqrt n\,t)$ . Practical codes nevertheless favour wide neighbourhoods, which allow long steps.

Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods $\mathcal N_\infty(\beta)$ and $\mathcal N_\infty^-(\beta)$ attains precision $t$ in $O(nt)$ iterations. With $\beta$ close to $1$ , $\mathcal N_\infty^-(\beta)$ contains almost all of the strictly feasible set.

Setting

Fix $n\ge1$ , $m\ge0$ , $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider

\text{(P)}\ \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad \text{(D)}\ \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .

The strictly feasible pairs $\mathcal F^0$ are the $(x,s)$ with $x>0$ , $s>0$ , $Ax=b$ , and $A^Ty+s=c$ for some $y$ . For such a pair the duality gap is $x^Ts$ , and the duality measure is $\mu=x^Ts/n$ . Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ and $e=(1,\dots,1)^T$ .

Norms: $\|\cdot\|$ is the Euclidean norm, $\|\cdot\|_\infty$ the maximum norm, and $\|z\|^-_\infty:=\|z^-\|_\infty$ , $\|z\|^+_\infty:=\|z^+\|_\infty$ with $(z^-)_j=\min\{z_j,0\}$ and $(z^+)_j=\max\{z_j,0\}$ . For $\beta\in(0,1)$ the wide neighbourhoods are

\mathcal N_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|_\infty\le\beta\mu\},\qquad \mathcal N^-_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|^-_\infty\le\beta\mu\}.

The second says only that $x_js_j\ge(1-\beta)\mu$ for every $j$ .

The search direction $d=(d_x,d_s)$ with centering parameter $\gamma$ solves, for some $d_y$ ,

Sd_x+Xd_s=\gamma\mu e-Xs,\qquad Ad_x=0,\qquad A^Td_y+d_s=0, \tag{2}

and the step is $x(\theta)=x+\theta d_x$ , $s(\theta)=s+\theta d_s$ . The scaled quantities $p=X^{-1/2}S^{1/2}d_x$ , $q=X^{1/2}S^{-1/2}d_s$ , $r=(XS)^{-1/2}(\gamma\mu e-Xs)$ satisfy $p+q=r$ and $p^Tq=0$ . The componentwise product $Pq=(p_jq_j)_j$ is the second-order term $D_xd_s$ .

Algorithm 2 with neighbourhood $\mathcal N$ and $\gamma\in(0,1)$ starts at $(x^0,s^0)\in\mathcal N$ with $(x^0)^Ts^0\le2^t$ . While $(x^k)^Ts^k>2^{-t}$ , it computes $d$ from (2), takes the largest $\bar\theta$ such that $(x(\theta),s(\theta))\in\mathcal N$ for all $\theta\in[0,\bar\theta]$ , and sets $(x^{k+1},s^{k+1})=(x(\bar\theta),s(\bar\theta))$ .

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Let $\beta,\gamma\in(0,1)$ with $\gamma\le2(1-\beta)$ , and let $\mathcal N$ be $\mathcal N_\infty(\beta)$ or $\mathcal N_\infty^-(\beta)$ . Every run of Algorithm 2 reaches $(x^k)^Ts^k\le 2^{-t}$ for some

k\ \le\ \Big\lceil\frac{\ln2\cdot n\,t}{2\beta\gamma(1-\gamma)}\Big\rceil .

The paper states " $O(nt)$ iterations"; the count above is the one its inequality (15) yields.

Milestones, in the order the proof uses them

Lemma 1(b): $-\|r\|^2/4\le p_jq_j\le r_j^2/4$ for each $j$ .
Lemma 1(c): $\|Pq\|^-_\infty\le\|r\|^2/4\le n\|r\|^2_\infty/4$ , $\|Pq\|^+_\infty\le\|r\|^2_\infty/4$ , $\|Pq\|_\infty\le\|r\|^2/4$ .
Lemma 2(c): if $\gamma\le2(1-\beta)$ and $(x,s)\in\mathcal N_\infty^-(\beta)$ then $\|r\|^2\le n\mu$ ; in $\mathcal N_\infty(\beta)$ , $\|r\|_\infty^2\le(1+\beta)\mu$ .
Lemma 5: $\bar\theta\ge\theta_2=\min\{1,\beta\gamma\mu/\|Pq\|_\infty\}$ in $\mathcal N_\infty(\beta)$ , and $\bar\theta\ge\theta_2^-=\min\{1,\beta\gamma\mu/\|Pq\|^-_\infty\}$ in $\mathcal N_\infty^-(\beta)$ .
Proof of Theorem 2: $\theta_2^-\ge\theta_2\ge4\beta\gamma/n$ (for $n\ge2$ ).
(15): $\mu^{k+1}\le\big(1-4\beta\gamma(1-\gamma)/n\big)\mu^k$ .

Significance

Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of $\mathcal F^0$ keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.

The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods $\mathcal N_\infty$ , $\mathcal N_\infty^-$ , of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.

Difficulty

Most of the steps are finite-dimensional inequalities. The sticking points are the following.

The bound $p_jq_j\ge-\|r\|^2/4$ uses the orthogonality $p^Tq=0$ , which comes from $Ad_x=0$ and $d_s=-A^Td_y$ . Those relations hold only for a solution of the full system (2), not for the first equation alone.
Lemma 5 needs every point of the segment $[0,\theta_2]$ to lie in the neighbourhood, including strict positivity of $x(\theta)$ and $s(\theta)$ and dual feasibility. Positivity of the products alone does not give positivity of the factors without a continuity argument along the segment.
"The largest $\bar\theta$ " is a maximum over a set defined by infinitely many conditions. The theorem needs only that $\bar\theta$ dominates $\theta_2$ , but the formal run must say what $\bar\theta$ is.
Converting the per-iteration contraction (15) into the explicit count needs $(1-\delta)^k\le e^{-k\delta}$ , real powers of $2$ , and a ceiling.

Formalization scope

Vectors are Fin n → ℝ, with coordinates indexed $0,\dots,n-1$ , and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. $\mu$ divides by $n$ as a real number. Here $\log$ is the natural logarithm and $2^t$ is a real power with $t\in\mathbb R$ .

Committed conventions and repairs:

The direction is "any $(d_x,d_y,d_s)$ solving (2)". No rank assumption on $A$ is made.
"The largest $\bar\theta$ " is IsGreatest of the set of admissible step lengths, and $\bar\theta$ is not capped at $1$ . When no maximum exists (always the case for $n=1$ , where $Pq=0$ ), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for $n=2$ .
A run is a pair of sequences that starts as required and makes one iteration from every iterate with $(x^k)^Ts^k>2^{-t}$ . Its behaviour after the stopping test is unconstrained.
In $\theta_2$ and $\theta_2^-$ , a zero norm makes the quotient $+\infty$ and the minimum $1$ . Since Lean's real division by zero is $0$ , this case is defined explicitly.
The bound $\theta_2\ge4\beta\gamma/n$ is stated for $n\ge2$ . At $n=1$ it can fail (e.g. $\beta=1/2$ , $\gamma=0.9$ ), and Algorithm 2 makes no iterations there.
The goal covers both neighbourhoods. A goal for $\mathcal N^-_\infty$ alone would be weaker than the paper.
Lemma 1 assumes only $x,s>0$ and $\gamma\in[0,1]$ of the pair, which is all its statement uses.

The goal is not to be read with a hidden constant. A statement of the form "there is $C$ with at most $Cnt$ iterations", with $C$ allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.

Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.

Selected references

S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944 (1990, rev. 1991); Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
M. Kojima, S. Mizuno, A. Yoshise, A primal-dual interior point algorithm for linear programming, in N. Megiddo (ed.), Progress in Mathematical Programming, Springer, 1989, pp. 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
R. D. C. Monteiro, I. Adler, Interior path following primal-dual algorithms. Part I: Linear programming, Mathematical Programming 44:27–41, 1989. https://doi.org/10.1007/BF01587075
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

11 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis Numerical Analysis+1·Captain: mikedeng1

Régularisation d'inéquations variationnelles par approximations successives II: The Proximal Regularization of a Convex Minimization Problem Is a Minimizing SequenceResearch Paper

Motivation

The proximal point algorithm replaces a hard optimization or equilibrium problem by a sequence of better-conditioned ones: from the current point $x^n$ it solves the original problem with a quadratic penalty $\|x-x^n\|^2$ added, and takes the solution as $x^{n+1}$ . The method is a building block of modern convex optimization. Augmented Lagrangian methods, Douglas–Rachford and ADMM splitting, and many bundle methods are proximal point iterations applied to suitable problems (Rockafellar 1976; Eckstein–Bertsekas 1992).

The algorithm was introduced by B. Martinet in a five-page note in the Revue française d'informatique et de recherche opérationnelle in 1970 (Martinet 1970). The note treats three cases: monotone variational inequalities on a bounded convex set (§II), convex–concave min–max problems (§III), and convex minimization (§IV). This mission formalizes §IV.

Timeline.

1970, Martinet: the regularization (13) for convex minimization over a closed convex set in a Hilbert space; Théorème 3 (weak cluster points are minimizers, the sequence is minimizing), stated without proof.
1976, Rockafellar (SIAM J. Control Optim. 14): the proximal point algorithm for maximal monotone operators, with inexact steps and weak convergence of the whole sequence when a zero exists.
1991, Güler (SIAM J. Control Optim. 29): the rate $f(x^n)-\inf f = O(1/n)$ for convex minimization, and an example in which the iterates converge weakly but not strongly.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $C\subseteq H$ be a nonempty, closed, convex set, and let $f:H\to\mathbb R$ be a convex, lower semicontinuous function such that, for every $a\in\mathbb R$ , the sublevel set $\{x\in C \mid f(x)\le a\}$ is bounded. These are the standing hypotheses of §4.1 (Lean: Standing f C). The problem is

(12)\qquad \min\,\{\,f(x)\mid x\in C\,\},

and its solution set (solSet f C) is the set of $\bar x\in C$ with $f(\bar x)\le f(x)$ for all $x\in C$ .

The regularization algorithm (13) starts from $x^0\in C$ and, given $x^n$ , takes

(13)\qquad x^{n+1}\in C\ \text{ the minimizer of } \ f(x)+\|x-x^n\|^2\ \text{ over } x\in C .

Lean encodes one step as IsProxStep f C xn y ( $y\in C$ and $f(y)+\|y-x^n\|^2\le f(x)+\|x-x^n\|^2$ for all $x\in C$ ) and a run as IsProxSeq f C x.

A point $\tilde x$ is a weak cluster point of $(x^n)$ (IsWeakClusterPt) if every neighbourhood of $\tilde x$ in the weak topology of $H$ contains $x^n$ for infinitely many $n$ . A sequence is minimizing if $f(x^n)\to\inf_{x\in C} f(x)$ .

Formalization targets

Existence for (12) and well-posedness of (13)

\exists\,\bar x\in C\ \ \forall x\in C:\ f(\bar x)\le f(x), \qquad \forall x^n\in C\ \ \exists!\,y\in C:\ y \text{ minimizes } f(x)+\|x-x^n\|^2 \text{ over } C .

These are the paper's claims in §4.1 ("Ces hypothèses assurent l'existence d'une solution pour (12)") and §4.2 ("solution unique").

Goal: Théorème 3

For every sequence generated by (13),

\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in \operatorname{sol}(12), \qquad \lim_{n\to\infty} f(x^n)=\inf_{x\in C} f(x)\in\mathbb R .

The goal asserts no rate and no constant. It is the statement the paper makes, with both conclusions in one theorem.

Stronger: Remarque 1

If in addition $f$ is uniformly convex, i.e. $f(ax+by)\le af(x)+bf(y)-ab\,\varphi(\|x-y\|)$ for $a,b\ge0$ , $a+b=1$ , with $\varphi(t)>0$ for $t>0$ , then (12) has a unique solution $\bar x$ and $\|x^n-\bar x\|\to0$ .

Significance

The result. Théorème 3 says that the proximal iterates make progress on the objective, not only on the distance to the solution set. A user of the method can stop on a value criterion. The convergence also needs no step-size tuning, no smoothness of $f$ , and no bound on $f$ beyond the boundedness of the sublevel sets. The well-posedness of (13) is what makes the method an algorithm. Each step is a strongly convex subproblem with a unique solution, and later inexact and splitting variants rely on that.

Formalizing it. The note gives no proof of Théorème 3 ("On peut faire une démonstration directe de ce théorème") and none of Remarque 1. The mission asks for a complete machine-checked proof of the convex minimization case of the original proximal point paper. To our knowledge, none of these statements has a machine-checked proof. Mathlib has convexity, lower semicontinuity, the weak topology of a normed space and uniform convexity of functions, but no proximal point algorithm.

Difficulty

Each iterate $x^{n+1}$ is defined only implicitly, as the minimizer of a problem that changes with $n$ . Monotonicity of $f(x^n)$ follows at once from comparing $x^{n+1}$ with $x^n$ . Monotonicity alone gives convergence of $f(x^n)$ to some limit, but not to $\inf_C f$ . Closing that gap needs information about the minimizers of (12) and their distance to the iterates.

The cluster-point statement is about the weak topology. A norm-continuity argument does not apply: $f$ is only lower semicontinuous in norm, and passing to weak limits requires the weak lower semicontinuity of convex lower semicontinuous functions. The boundedness that makes weak cluster points exist comes from the sublevel-set hypothesis, not from $C$ , which may be unbounded.

Formalization scope

All statements live in MartinetReg.ConvexMin. The conventions the formalization commits to:

$H$ is a real complete inner product space (InnerProductSpace ℝ H, CompleteSpace H). The paper says "espace de Hilbert", and its inequalities make it real.
$C\neq\emptyset$ is a standing hypothesis. The paper leaves it implicit, but its existence claim for (12) is false for $C=\emptyset$ .
$f$ is real-valued, convex and lower semicontinuous on all of $H$ , as printed. The constraint $x\in C$ stays explicit in (12) and (13). It is not absorbed into an extended-valued indicator.
The penalty in (13) has weight $1$ , as printed, not $\tfrac12$ .
The algorithm is a relation on sequences: IsProxSeq accepts any sequence with $x^0\in C$ satisfying (13) at every step. Existence and uniqueness of the step are a separate milestone, not built into a definition by choice.
"Minimisante" is stated as: some real $m$ is the greatest lower bound of $f(C)$ and $f(x^n)\to m$ . This avoids the junk value sInf takes on sets unbounded below. As a side effect, the theorem asserts that $f$ is bounded below on $C$ .
Weak cluster points are cluster points in WeakSpace ℝ H. A norm cluster point would weaken the conclusion and is not used.
Remarque 1 uses Mathlib's UniformConvexOn Set.univ φ f with $\varphi(t)>0$ for $t>0$ . It keeps every hypothesis of §4.1.

The goal does not assume that (12) has a solution, that $f$ is bounded below on $C$ , or that the iterates are bounded. Each of these would remove part of the content of Théorème 3, and the first two are consequences proved as milestones.

Not formalized here: Remarque 2 (p. 158), a comment that convexity seems indispensable; and the Exemple (p. 158). The Exemple's linear system $(A^*A+2I)x^{n+1}=A^*b+2x^n$ corresponds to $f=\tfrac12\|Ax-b\|^2$ . For the printed $f=\|Ax-b\|^2$ , (13) gives $(A^*A+I)x^{n+1}=A^*b+x^n$ . The variational inequality case (§II) is the companion mission I of this series.

Reusable beyond this mission: the existence of minimizers of convex lower semicontinuous functions with bounded sublevel sets on closed convex subsets of a Hilbert space, and the weak lower semicontinuity it rests on. Contributions of these general lemmas, and of strong-convexity facts for $x\mapsto f(x)+\|x-x^n\|^2$ , are welcome.

Selected references

B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3), 154–158, 1970. https://doi.org/10.1051/m2an/197004R301541
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14(5), 877–898, 1976. https://doi.org/10.1137/0314056
O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29(2), 403–419, 1991. https://doi.org/10.1137/0329022
J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Mathematical Programming 55, 293–318, 1992. https://doi.org/10.1007/BF01581204
J. L. Lions and G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20, 493–519, 1967. https://doi.org/10.1002/cpa.3160200302

6 thms3 active usersReviewed

Completed

Linear algebra Operations Research·Captain: mikedeng1

Strongly Regular Generalized Equations IV: Strong Second-Order Sufficiency and Linearly Independent Binding Gradients Make the KKT Generalized Equation Strongly RegularResearch Paper

Motivation

A nonlinear program is rarely solved once. Its data are estimated, rounded, or varied on purpose in a parametric study, and an algorithm such as sequential quadratic programming replaces it at every iteration by a nearby linearised problem. Both uses need the same fact: near a solution, the Karush–Kuhn–Tucker (KKT) system should have exactly one solution for every small perturbation, and that solution should move Lipschitz-continuously with the perturbation. For problems with equality constraints only, or with strict complementary slackness, the classical implicit-function theorem gives this, as in Fiacco's sensitivity analysis (Fiacco 1976, reference [4] of the paper). Without strict complementarity the KKT system is not a smooth equation, and the classical theorem does not apply.

S. M. Robinson's paper Strongly regular generalized equations, Math. Oper. Res. 5 (1980) 43–62 introduced strong regularity to handle exactly this case. §2 of the paper proves an implicit-function theorem for generalized equations, §3 characterises strong regularity of linear generalized equations through a Schur complement, and §4, the subject of this mission, applies both to nonlinear programming. Its Theorem 4.1 identifies the conditions under which the KKT system is strongly regular. These conditions (strong second-order sufficiency and linearly independent binding gradients) became standard hypotheses in the stability theory of nonlinear programs and in the local convergence analysis of Newton-type methods.

Setting

Let $\Omega\subseteq\mathbb R^n$ be open and let $\theta:\Omega\to\mathbb R$ , $g:\Omega\to\mathbb R^p$ , $h:\Omega\to\mathbb R^q$ be Fréchet differentiable. The program is

\text{minimize } \theta(x)\quad\text{subject to}\quad g(x)\le0,\ h(x)=0.\qquad(4.1)

The Lagrangian is $\mathcal L(x,u,v)=\theta(x)+\langle u,g(x)\rangle+\langle v,h(x)\rangle$ , and $\mathcal L'$ is its gradient in $x$ .

For a set $C$ and a point $z$ , the normal-cone operator $\partial\psi_C(z)$ is the set of vectors $y$ with $\langle y,c-z\rangle\le0$ for all $c\in C$ when $z\in C$ , and the empty set when $z\notin C$ . The KKT conditions of (4.1) are the generalized equation

0\in F(x,u,v)+\partial\psi_{\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q}(x,u,v),\qquad F(x,u,v)=\big(\mathcal L'(x,u,v),\,-g(x),\,-h(x)\big).\qquad(4.3)

Its middle block says $g(x)\le0$ , $u\ge0$ and $\langle u,g(x)\rangle=0$ .

A generalized equation $0\in F(z)+\partial\psi_C(z)$ is strongly regular at a solution $z_0$ (DEFINITION, p. 45) if its linearisation $T(z)=F(z_0)+F'(z_0)(z-z_0)+\partial\psi_C(z)$ satisfies the following. There are neighbourhoods $U$ of $0$ and $V$ of $z_0$ and a constant $\lambda$ such that, for every $y\in U$ , the inclusion $y\in T(z)$ has exactly one solution $z=s(y)$ in $V$ , and $s$ is $\lambda$ -Lipschitz on $U$ .

At a solution $(x_0,u_0,v_0)$ the inequality constraints split into three groups:

$g^+$ , with $g_i(x_0)=0$ and $u_{0,i}>0$ ;
$g^0$ , the weakly active ones, with $g_i(x_0)=0=u_{0,i}$ ;
$g^-$ , with $g_i(x_0)<0$ .

Write $\mathcal L''=\mathcal L''(x_0,u_0,v_0)$ for the Hessian of the Lagrangian in $x$ , $H=h'(x_0)$ , $G^+=g^{+\prime}(x_0)$ and $G^0=g^{0\prime}(x_0)$ . A square matrix is a P-matrix if all its principal minors are positive.

Formalization targets

Goal: Theorem 4.1 (p. 56)

Assume $\theta,g,h$ are twice differentiable at $x_0$ and $(x_0,u_0,v_0)$ solves (4.3). Assume also:

(a′) strong second-order sufficiency: $\langle y,\mathcal L''y\rangle>0$ for all $y\ne0$ with $G^+y=0$ and $Hy=0$ ;
(b) linear independence: the matrix $\begin{bmatrix}G^+\\G^0\\H\end{bmatrix}$ has full row rank.

Then

\text{(4.3) is strongly regular at }(x_0,u_0,v_0).

The Lipschitz constant is not fixed; the goal asserts that one exists.

Milestones

The matrix $K=\begin{bmatrix}\mathcal L''&H^T&G^{+T}\\-H&0&0\\-G^+&0&0\end{bmatrix}$ of (4.5) is nonsingular.
The equations (4.8) define $V,A,B$ uniquely, and the Schur complement $S=[G^0\ 0\ 0]\,K^{-1}\,[G^0\ 0\ 0]^T$ of (4.6) satisfies $S=G^0V=V^T\mathcal L''V$ , so $S$ is symmetric.
A symmetric matrix is a P-matrix if and only if it is positive definite.
$S$ is positive definite.
The §4 criterion (p. 55): (4.3) is strongly regular at $(x_0,u_0,v_0)$ if and only if $K$ is nonsingular and $S$ is a P-matrix.

A further item formalizes the example (4.9)–(4.10) on pp. 56–57: a linear generalized equation in $\mathbb R^4$ whose unique solution satisfies the ordinary second-order sufficient condition and (b), yet is not strongly regular.

Significance

Strong regularity is the hypothesis of Robinson's implicit-function theorem (Theorem 2.1 of the paper). Theorem 4.1 therefore yields, for a parametrised nonlinear program, a locally unique and Lipschitz-continuous KKT point together with its multipliers, without strict complementary slackness. The same property underlies the local quadratic convergence of Josephy–Newton and SQP methods, and the criterion of milestone 5 is the form in which it is usually checked. The example of (4.10) shows that the ordinary second-order sufficient condition is not enough; the weakly active constraints have to be dropped from the cone on which $\mathcal L''$ must be positive.

All statements are proved in the paper. None of them, nor the notion of strong regularity, has a machine-checked proof on this platform. The matrix milestones (1–4) are self-contained linear algebra and can be proved independently. Milestone 3 for arbitrary symmetric matrices is a variant of Sylvester's criterion, which Mathlib does not currently state. Milestone 5 rests on §3 and the appendix of the paper (the Schur-complement criterion and the reduction of a linear generalized equation over a polyhedral set), which are the subjects of the companion missions II and III of this series.

Difficulty

The obvious argument would apply the classical implicit-function theorem to the active KKT equations. It fails because of the weakly active constraints. Near $(x_0,u_0,v_0)$ a constraint with $g_i(x_0)=0=u_{0,i}$ can become active or inactive under arbitrarily small perturbations, so the solution map is piecewise smooth, not smooth. Uniqueness has to hold across all the pieces simultaneously, which is a combinatorial condition: the P-matrix property of a Schur complement, not the nonsingularity of a single Jacobian. Example (4.10) shows that the natural guess (nonsingularity of every piece, guaranteed by ordinary second-order sufficiency) is insufficient: three distinct KKT points can coalesce at the origin.

The analytic part is also not routine. Strong regularity concerns the linearised problem with an arbitrary small perturbation on the right-hand side, including perturbations of the complementarity block. The criterion needs the reduction of §3 and the appendix, which localises the polyhedral set $\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q$ around the solution.

Formalization scope

Spaces. Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n). The triple $(x,u,v)$ lives in EuclideanSpace ℝ (Fin n ⊕ (Fin p ⊕ Fin q)), the Euclidean $\mathbb R^{n+p+q}$ , so the normal cone uses the standard inner product. A product type, which carries the sup norm and no inner product, is deliberately not used.
Normal cone. The operator includes the clause $z\in C$ , so it is empty off $C$ .
Strong regularity. It is stated on the linearisation data, with a real Lipschitz constant $\lambda$ , and requires existence, uniqueness in $V$ and the Lipschitz bound. Strong regularity at a point bundles a Fréchet derivative of $F$ there.
Twice differentiable at $x_0$ . This is encoded as $\theta$ , $g_i$ , $h_j$ differentiable on the open set $\Omega$ (the standing assumption of (4.1)), together with differentiability at $x_0$ of their gradients. It is not $C^2$ on $\Omega$ , and symmetry of $\mathcal L''$ is not assumed; it follows.
Matrix conventions. Positive definite means $\langle w,Mw\rangle>0$ for $w\ne0$ , without symmetry. P-matrix quantifies over all nonempty principal index sets. The Schur complement is used only together with nonsingularity of (4.5), because Mathlib's inverse of a singular matrix is $0$ .
What must not be formalized. Replacing (a′) by the ordinary second-order sufficient condition, or restricting (b) to $G^+$ and $H$ , gives a false or a different theorem. The milestones state exactly which constraints enter each condition: (a′) uses $G^+$ and $H$ , and (b) uses $G^+$ , $G^0$ and $H$ . A formalization that drops the weakly active constraints from (b), or assumes strict complementarity, trivializes the goal to the classical implicit-function theorem.
Infrastructure. A complete development needs the normal cone of a product of orthants, block-matrix inversion and Schur-complement identities, Sylvester-type criteria for symmetric matrices, and the reduction of a linear generalized equation over a polyhedral set to its reduced form. The linear-algebra milestones are reusable beyond this mission. Proofs of any milestone, and of the general P-matrix/positive-definite equivalence, are welcome.

Selected references

S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1) (1980) 43–62. https://doi.org/10.1287/moor.5.1.43
A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968 (reference [3] of the paper; second-order sufficient condition, Chapter 2).
A. V. Fiacco, Sensitivity analysis for nonlinear programming using penalty methods, Mathematical Programming 10 (1976) 287–311 (reference [4] of the paper). https://doi.org/10.1007/BF01580379
R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8 (1974) 189–211 (reference [1] of the paper). https://doi.org/10.1016/0024-3795(74)90055-4
A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014 (modern account of strong regularity). https://doi.org/10.1007/978-1-4939-1037-3

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 3: Shifting and Scaling the Processing Times Changes Neither the Optimal Sequence nor the Branch-and-Bound PathResearch Paper

Motivation

Branch and bound was introduced for integer programming by Land and Doig (1960) and for the travelling salesman problem by Little, Murty, Sweeney and Karel (1963). Ignall and Schrage (1965) were among the first to apply it to machine scheduling. They give lower bounds for two permutation flow-shop problems: the makespan on three machines, and the mean completion time on two. Their Appendix then asks how the method depends on the units and the origin of the data. Its THEOREM says that changing the location and the scale of all processing times changes neither the optimal sequence nor the path the branch-and-bound procedure takes.

The statement matters for computational experiments of the kind the paper reports. Run times and node counts measured on one jobset carry over to every jobset obtained from it by a positive affine change of the processing times, so a test family need only vary the shape of the data, not its location and scale. It is also a correctness property of the procedure: a branch-and-bound method whose behaviour depended on the time unit would be suspect.

Setting

There are $n$ jobs, and every job visits the machines in the same order: $A$ , then $B$ (two-machine problem), or $A$ , $B$ , then $C$ (three-machine problem). Job $i$ has nonnegative processing times $a_i, b_i$ (and $c_i$ ). Following Johnson (1954), both problems are restricted to permutation schedules. A full sequence $\sigma$ lists the jobs in the order in which every machine processes them, and each operation starts as early as possible. The makespan of $\sigma$ is the time machine $C$ finishes its last job. The completion time $d_i$ of job $i$ is the time machine $B$ finishes it, and the two-machine objective is $\sum_i d_i$ , which is $n$ times the mean completion time.

A node $J_r$ is a partial sequence of $r$ distinct jobs, and $\bar J_r$ is the set of the $n-r$ jobs it has not scheduled. For three machines, $\mathrm{TIMEA}, \mathrm{TIMEB}, \mathrm{TIMEC}(J_r)$ are the times the machines finish $J_r$ , and the lower bound (p. 401) is

LB(J_r)=\max\Big[\mathrm{TIMEA}+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}+\sum_{\bar J_r}c_i\Big].

For two machines, $\hat T_r$ and $\hat S_r$ are the minima over orderings of $\bar J_r$ of two explicit sums $T_r$ , $S_r$ (pp. 405–406), and the lower bound is $LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r)$ .

The branch-and-bound procedure (p. 402) keeps a list of nodes ranked by $LB$ , starting from the root alone. At each step it removes the first node and inserts each of its children $J_r\,j$ ranked into the list. On ties a new node goes before an old one (p. 403). It stops when the first node has scheduled $n-1$ jobs, which fixes the whole sequence. The list after $k$ steps is $\mathrm{run}_{LB}(k)$ .

Problems $P'$ (data $a'_i,b'_i,c'_i$ ) and $\tilde P$ are related by a change of location and scale when

\tilde a_i = H(a'_i+G),\qquad \tilde b_i=H(b'_i+G),\qquad \tilde c_i = H(c'_i+G),\qquad H,G>0.

Formalization targets

Goal: the Appendix THEOREM (p. 411)

For both the three-machine makespan problem and the two-machine sum-of-completion-times problem:

\sigma \text{ is optimal for } \tilde P \iff \sigma \text{ is optimal for } P', \qquad \mathrm{run}_{LB_{\tilde P}}(k)=\mathrm{run}_{LB_{P'}}(k)\ \text{ for all } k .

Milestones, in the order of the paper's proof

Adding $G$ to every processing time raises the completion time of the $r$ -th job on machine $M$ by $G(r+M-1)$ .
On two machines, $\sum_i d_i$ rises by $\tfrac12 Gn(n+3)$ for every sequence.
On two machines, $\hat T_r$ and $\hat S_r$ rise by $G[r(n-r)+\tfrac12(n-r)(n-r+1)+(n-r)]$ , $\sum_{J_r}d_i$ by $\tfrac12Gr(r+3)$ , and $LB(J_r)$ by $\tfrac12Gn(n+3)$ , for $1\le r\le n-1$ .
On three machines, every makespan and every $LB(J_r)$ with $1\le r\le n-1$ rises by $G(n+2)$ .
Multiplying all processing times by $H>0$ multiplies all these quantities by $H$ .
If $LB'=\varphi\circ LB$ on the nodes with $1\le r\le n-1$ , for a strictly increasing $\varphi$ , the two runs coincide at every step.

Significance

The THEOREM makes the method's behaviour a function of the shape of the data alone, not of its location or scale. This justifies normalizing test data, comparing running times across jobsets that differ by a change of units, and reporting results for one representative of each class. The proof also isolates a general principle: a deterministic best-first search depends on its bound only through the order the bound induces on the nodes it compares. Milestone 6 states that principle for the procedure of p. 402 with an arbitrary bound, so it applies to any other bound plugged into the same procedure.

As far as is known, no machine-checked version of this result or of the two lower bounds exists. The formalization needs the paper's procedure, with its tie rule, as an explicit deterministic function, and both lower bounds as functions of a node. The mission produces both, along with exact shift identities for every quantity the procedure uses.

Difficulty

The obvious argument is "adding $G$ adds a constant to everything", and it is not literally true. The constant depends on the position of a job and on the machine, so the identities must be computed term by term: maxima over machine-availability times commute with the shift only because both arguments move by the same amount, and that fails at the first job if processing times may be negative. The paper's own accounting contains a slip, the missing factor $G$ in $\tfrac12 r(r+3)$ . Its claim that "all lower bounds" of the three-machine problem rise by $G(n+2)$ is false at the root, where $\mathrm{TIMEB}=0$ does not move. The run equality therefore has to use the fact that the root is never compared with another node. The minima $\hat T_r$ , $\hat S_r$ range over all orderings of $\bar J_r$ , so their shift requires every ordering to move by the same amount. Finally, "the same path" has to be shown for the procedure's insertion with ties, step by step.

Formalization scope

Jobs are Fin n, numbered from $0$ . Processing times are real, and the shift statements and the goal assume them nonnegative, the paper's standing convention for durations. With negative times the goal is false (a three-job counterexample is recorded in the goal's statement). Scaling needs no sign condition.
The schedules of full sequences are Johnson's published as-soon-as-possible schedules (JohnsonFlowShop.ThreeStage.asapDone, JohnsonFlowShop.TwoStage.asapC2). Node attributes are computed by the same recursion on lists.
The two-machine objective is $\sum_i d_i$ instead of the mean; the two have the same minimizers.
$\hat T_r$ and $\hat S_r$ are minima over all orderings of $\bar J_r$ , not values at a sorted order.
Terminal nodes have depth $n-1$ . The procedure inserts children one at a time in increasing job index, each before every node of equal bound. Dominance discarding is not part of it.
Explicit readings. "The same sequence is optimal for both problems" means the sets of optimal sequences are equal, stated as an iff for every $\sigma$ . "Will follow the same path" means $\mathrm{run}(k)$ is equal for both problems at every $k$ . The paper's "all lower bounds" in the three-machine shift is restricted to nodes with $1\le r\le n-1$ . The hypotheses $H>0$ and $G>0$ are kept as stated.
Trivializations ruled out. A goal asserting only that some common optimal sequence exists, or only that the optimal values are related, would be weaker than the THEOREM. The goal states the iff and the equality of runs, with the procedure fixed independently of the data except through the bound.
The procedure, the node attributes and the lower bounds are also drafted in missions 1 and 2 of this series. Milestone 6 is reusable for any bound used with the same procedure. Proofs of any milestone are welcome. Generalizations, such as arbitrary real $G$ in the shift identities, are welcome as separate items.

Credit: Johnson (1954) for the reduction to permutation schedules and the published schedule definitions. No platform item treats flow-shop lower bounds or branch and bound over sequences. The nearest is the branch-and-bound mission BiconvexProg.BranchBound (Al-Khayyal and Falk), an unrelated algorithm for biconvex programs.

Selected references

E. Ignall, L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
A. H. Land, A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
J. D. C. Little, K. G. Murty, D. W. Sweeney, C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 972–989, 1963. https://doi.org/10.1287/opre.11.6.972

15 thms3 active usersReviewed

Machine Learning Operations Research Probability·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 1: AIM's Average Expected Cost Is Within O(1/√T) of the Newsvendor Cost, Perishable and Non-PerishableResearch Paper

Motivation

A retailer who restocks a product every period must choose an order-up-to level without knowing the demand distribution, and in most retail settings it observes only sales, the minimum of demand and stock. Demand above the stock is lost and never recorded. This is censored demand: the data needed to estimate the distribution are truncated exactly at the decision. Classical inventory theory assumes the distribution is known, and then the optimal policy in the stationary case is to order up to the newsvendor quantity in every period.

Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) give a nonparametric policy that learns from censored sales alone, the Adaptive Inventory Management (AIM) algorithm, and prove that its average expected cost approaches the newsvendor cost at rate $1/\sqrt T$ . The perishable case reduces to online convex optimization in the sense of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). The non-perishable case is new: leftover stock constrains the next decision, and the paper controls this constraint through a single-server queue.

Setting

Demands $D_1, D_2, \dots \ge 0$ are independent and identically distributed with an unknown law of finite mean; $D$ denotes a generic demand and $F$ its distribution function. A holding cost $h > 0$ is paid per unit left over and a penalty $b > 0$ per unit of lost demand. The newsvendor cost of a level $y \ge 0$ is

Q(y) = h\,E[y-D]^+ + b\,E[D-y]^+ ,

and the newsvendor quantity is $y^{NV} = \inf\{y \ge 0 \mid F(y) \ge b/(b+h)\}$ .

In period $t$ the manager holds $x_t \ge 0$ units ( $x_1 = 0$ ), raises the stock to $y_t \ge x_t$ , and observes $\min\{D_t, y_t\}$ . Excess inventory is either perishable ( $x_{t+1} = 0$ ) or non-perishable ( $x_{t+1} = [y_t - D_t]^+$ ).

Assumption 1 gives the manager a bound $\bar y \ge y^{NV}$ , and in the non-perishable case a bound $\rho$ with $0 < \rho < E[D_1]$ . AIM keeps a target $\hat y_t$ and an implemented level $y_t$ : $y_1 = \hat y_1 \in [0, \bar y]$ , and for $t \ge 1$

\hat y_{t+1} = P_{[0,\bar y]}\big(\hat y_t - \epsilon_t H_t(\hat y_t)\big), \qquad y_{t+1} = \max\{\hat y_{t+1}, x_{t+1}\},

with the projection $P_{[0,\bar y]}(z) = \max\{\min\{z,\bar y\},0\}$ , steps $\epsilon_t = \gamma\bar y/(\max\{b,h\}\sqrt t)$ for a scale $\gamma > 0$ , and the censored gradient estimate $H_t(\hat y_t) = h$ if $D_t < \hat y_t$ and $-b$ if $D_t \ge \hat y_t$ . The manager can compute $H_t$ from the observed sales.

For $\theta > 0$ the waiting times $W_1(\theta) = 0$ , $W_{t+1}(\theta) = [W_t(\theta) + \theta - D_t]^+$ describe a GI/D/1 queue with inter-arrival times $D_t$ and service time $\theta$ . Its busy periods $J_i(\theta)$ are the stretches between successive returns to $0$ . The auxiliary queue $Z_1(\theta) = 0$ , $Z_{t+1}(\theta) = [Z_t(\theta) + \theta/\sqrt t - D_t]^+$ has shrinking service times.

Formalization targets

Goal: Theorem 2

For every $T \ge 1$ , in the perishable case

E\Big[\frac1T\sum_{t=1}^T Q(y_t)\Big] - Q(y^{NV}) \le \Big(\gamma + \frac1\gamma\Big)\frac{\bar y\max\{b,h\}}{\sqrt T},

and in the non-perishable case, if $E[D_1^6] < \infty$ and $\gamma \le \rho\max\{b,h\}/(h\bar y)$ , there is a constant $C$ , independent of $T$ , with

E\Big[\frac1T\sum_{t=1}^T Q(y_t)\Big] - Q(y^{NV}) \le \frac{C}{\sqrt T}.

The non-perishable bullet asserts only the existence of $C$ , because the paper's explicit formula (9) depends on Proposition 4 (i), which is false as printed.

Milestones

§2.4: $Q$ is convex with left derivative $h P\{D<y\} - bP\{D\ge y\}$ , and $E[H_t \mid \hat y_t]$ equals it.
Lemma 3: projected stochastic subgradient descent with steps $\gamma\operatorname{diam}(S)/(\bar B\sqrt t)$ has average error at most $(\gamma + 1/\gamma)\operatorname{diam}(S)\bar B/\sqrt T$ .
§2.4: $Q(y) - Q(\hat y) \le h(y - \hat y)$ for $0 \le \hat y \le y$ .
Theorem 6: if $\gamma \le \rho\max\{b,h\}/(h\bar y)$ , then $y_t - \hat y_t \le Z_t(\rho)$ .
Lemma 13: $E|J_{i(\theta,t)}(\theta)| \le E[|J_1(\theta)|^2]$ .
Lemma 5: $E[\sum_{t=1}^T Z_t(\theta)] \le 2\theta E[|J_1(\theta)|^2]\sqrt T$ .
Lemma 12: $E[(\sum_{i\le n} X_i)^6] \le 21 n^3 E X_1^6$ for i.i.d. mean-zero $X_i$ (and the fourth-moment analogue).
Proposition 4 (i), corrected: $E[|J_1(\theta)|^2] \le 1 + \tfrac{21\pi^2}{2}E[(D_1 - ED_1)^6]/(ED_1 - \theta)^6$ for $0 < \theta < E[D_1]$ .

Significance

Theorem 2 shows that a manager who never observes lost sales can still reach the cost of a manager who knows the distribution, at a dimension-free rate, under only a sixth-moment condition in the non-perishable case. The example of §2.5 of the paper shows that the rate $1/\sqrt T$ cannot be improved in general for AIM. Theorem 6, the coupling of the excess inventory $y_t - \hat y_t$ with a queue, is the step that handles decisions constrained by past decisions, and the same paper reuses it when $\rho$ is unknown (§3.2).

The results are proved in the paper, and none of them is formalized as far as is known. This mission formalizes them and also corrects them: Proposition 4 (i) fails for deterministic demand, its explicit constant has to be replaced, and Eq. (2) labels a right derivative as a left one. Lemma 3 for decreasing steps and Lemma 12 are standard tools that are not in Mathlib.

Difficulty

The perishable case is a stochastic subgradient method, but its estimates are conditionally unbiased only given the current iterate, and $Q$ is merely convex, not differentiable, so the textbook smooth argument does not apply directly. In the non-perishable case the implemented levels $y_t$ are not the gradient iterates, and $y_t - \hat y_t$ is not small along a path: carried-over stock can keep $y_t$ above the target for many periods. A bound on $E[y_t - \hat y_t]$ for each $t$ does not follow from a bound on one period. The queue $Z_t(\rho)$ dominates the whole excess process, but it is non-stationary. Its sum has to be compared with the stationary queue $W_t(\rho)$ , whose busy period covering a fixed time is length-biased, so second moments of busy periods enter.

Formalization scope

All declarations are in the namespace AIMInventory.Known. The demand law and the i.i.d. path measure are the published CappedBaseStock.DemandLaw and demandPathLaw, whose law has finite and strictly positive mean. $Q$ and $y^{NV}$ are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. The optimality of $y^{NV}$ is the already posed LostSalesOrderUpTo.Asymptotic.newsvendor_optimal and is included as a reference.

Conventions:

The demand path is zero-based ( $D_t$ is d (t - 1)), and all paper indices $t \ge 1$ are kept.
The AIM run, $W$ , $Z$ , the renewal epochs and the busy periods are functions of the demand path, defined by recursion exactly as printed.
The queue indexing is $W_1 = Z_1 = 0$ and $\tau_0 = 1$ (the paper's $W_0$ , $Z_0$ need an undefined $D_0$ and $\theta/\sqrt 0$ ). Period $1$ lies in no busy period, so Lemma 13 is stated for $t \ge 2$ .
Busy-period lengths are ℕ∞-valued. Every expectation that can be infinite is a lower Lebesgue integral in $[0,\infty]$ . The expectations in Theorem 2 have bounded integrands.
Readings of loose phrases:
- "for some $\gamma > 0$ " means for every $\gamma > 0$ ;
- "any value in $[0,\bar y]$ " means for every $\hat y_1 \in [0, \bar y]$ ;
- "with probability one" in Theorem 6 means for every demand path;
- "There is a constant $C$ " means $\exists C,\ \forall T \ge 1$ .
The implicit positivity of $h$ , $b$ , $\bar y$ (they appear in denominators) is added as hypotheses.
Lemma 3 is stated on $\mathbb R^n$ for every comparator $u \in S$ , with $E[H(z)\mid z]$ read as conditioning on the σ-algebra of the current iterate.
Proposition 4 (ii) and the explicit constant (9) are not stated.

The mission does not accept a formalization that sums over arbitrary sequences with $y_t \ge \hat y_t$ instead of the AIM run, uses an uncensored gradient, or lets a non-integrable expectation default to $0$ .

Contributions toward a stochastic subgradient method with anytime steps, moment bounds for i.i.d. sums, and busy periods of Lindley's recursion are reusable beyond this mission.

Selected references

W. T. Huh, P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1), 2009. https://doi.org/10.1287/moor.1080.0355
M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
A. Flaxman, A. T. Kalai, H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
E. Hazan, A. Agarwal, S. Kale, Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8

15 thms3 active usersReviewed

Machine Learning Operations Research Probability·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 3: For Any Step Scale γ, Non-Perishable AIM's Excess Cost Λ₂(T) Is Bounded by a Hitting Time and a Busy PeriodResearch Paper

Motivation

A retailer who stocks a perishable or storable product each period must choose an order-up-to level without knowing the demand distribution. Worse, demand is censored: when the shelf empties, the retailer observes sales, not demand. Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) proposed the Adaptive Inventory Management (AIM) algorithm, a projected stochastic subgradient method that uses only the censored observation "was there stock left at the end of the period?". They proved that its average expected cost converges to the cost of the optimal newsvendor level at rate $O(1/\sqrt T)$ , with no parametric assumption on demand.

In the non-perishable case, where leftover stock carries over, the main convergence theorem (Theorem 2, p. 7) requires the step-size scale $\gamma$ to satisfy $\gamma\le\rho\max\{b,h\}/(h\bar y)$ , where $\rho$ is a known lower bound on mean demand. Section 3.2 of the paper removes this requirement. Its Theorem 8 bounds the excess cost of AIM for every step scale $\gamma>0$ , at the price of a hitting time and a busy period in the bound. This mission formalizes Theorem 8 and the steps of its proof.

Setting

Demands $D_1,D_2,\dots$ are independent, nonnegative, identically distributed, with finite positive mean $E[D_1]$ and otherwise unknown law. The holding cost is $h>0$ per unit left over and the penalty is $b>0$ per unit of unmet demand. The newsvendor cost of stocking up to $y\ge0$ is

Q(y)=h\,E[y-D_1]^+ + b\,E[D_1-y]^+ ,

and the newsvendor quantity is $y^{NV}=\inf\{y\ge0: P(D_1\le y)\ge b/(b+h)\}$ . The manager knows an upper bound $\bar y\ge y^{NV}$ .

AIM, non-perishable case. Fix $\gamma>0$ and a starting target $\hat y_1\in[0,\bar y]$ . Put $y_1=\hat y_1$ , $x_1=0$ . In period $t\ge1$ the step is $\epsilon_t=\gamma\bar y/(\max\{b,h\}\sqrt t)$ , the observed slope is $H_t=h$ if $D_t<\hat y_t$ and $H_t=-b$ otherwise, and

\hat y_{t+1}=\max\{\min\{\hat y_t-\epsilon_tH_t,\bar y\},0\},\qquad x_{t+1}=[y_t-D_t]^+,\qquad y_{t+1}=\max\{\hat y_{t+1},x_{t+1}\}.

The target $\hat y_t$ follows the gradient step. The implemented level $y_t$ can exceed it because stock that has already been bought cannot be returned. The excess-cost term is

\Lambda_2(T)=E\Big[\frac1T\sum_{t=1}^T\big(Q(y_t)-Q(\hat y_t)\big)\Big].

Auxiliary processes. Let $m=h\gamma\bar y/\max\{b,h\}$ . For a real $\theta$ :

$W_1(\theta)=0$ , $W_{t+1}(\theta)=[W_t(\theta)+\theta-D_t]^+$ is a queue with constant inflow. Its first busy period has length $|J_1(\theta)|=\inf\{t>1:W_t(\theta)=0\}-1$ .
$Z_1(\theta)=0$ , $Z_{t+1}(\theta)=[Z_t(\theta)+\theta/\sqrt t-D_t]^+$ is a queue with decreasing inflow.
$K(\theta,z)=\min\{t\ge0: z+\sum_{s=1}^t(\theta-D_s)\le0\}$ is the hitting time of $(-\infty,0]$ by the random walk started at $z$ .

For $0<\rho'<m$ , the proof uses $\tilde T=\lceil(m/\rho')^2\rceil$ and $\tilde K=\min\{t>\tilde T:Z_t(m)=0\}$ .

Formalization targets

Goal: Theorem 8 (p. 13)

For every $T\ge1$ and every $\rho'$ with $0<\rho'<\min\{m,E[D_1]\}$ ,

\Lambda_2(T)\le\frac{\max\{b,h\}\,\bar y}{T}\Big\{\big\lceil(m/\rho')^2\big\rceil+E\Big[K\Big(\rho',\frac{2\sqrt2\,m^2}{\rho'}\Big)\Big]\Big\}+\frac{2hm\,E\big[|J_1(\rho')|^2\big]}{\sqrt T}.

The statement makes no moment assumption on demand. It is stated with the paper's explicit constants, and both expectations on the right may be infinite.

Milestones

Coupling (proof of Theorem 8, p. 13). For every demand path and every $t\ge1$ , $y_t-\hat y_t\le Z_t(m)$ .
Restart bound (p. 14). For $0<\rho'<m$ , $E[\tilde K]\le\lceil(m/\rho')^2\rceil+E[K(\rho',2\sqrt2m^2/\rho')]$ .
Claim (14) (p. 14, proved in Appendix E). For $0<\rho'<\min\{m,E[D_1]\}$ , $\frac hT E\big[\sum_{t=\tilde K+1}^T Z_t(m)\big]\le 2hm\,E[|J_1(\rho')|^2]/\sqrt T$ .
Lemma 9, corrected (p. 13). If $\theta<E[D_1]$ , $E[D_1^4]<\infty$ and $z>0$ , then $E[K(\theta,z)]\le1+\frac{2z}{E[D_1]-\theta}+\frac{8\pi^2E[(D_1-E[D_1])^4]}{(E[D_1]-\theta)^4}$ .

Significance

The result. The cost of AIM relative to the newsvendor benchmark splits as $\Lambda_1(T)+\Lambda_2(T)$ . Stochastic subgradient descent controls $\Lambda_1(T)$ for every $\gamma$ , so Theorem 8 is the remaining step in showing that AIM converges at rate $O(1/\sqrt T)$ without any knowledge of a lower bound on mean demand. The first term of the bound is $O(1/T)$ whenever $E[K]$ is finite, and Lemma 9 gives that under a finite fourth moment. The second term is $O(1/\sqrt T)$ whenever $E[|J_1|^2]$ is finite, and the paper's Proposition 4 gives that under a finite sixth moment. The result therefore removes the one piece of prior information about demand, other than $\bar y$ , that the non-perishable analysis needed.

Formalizing it. The paper's proof is complete and short, but it moves between expectations of random indices, pathwise couplings and renewal arguments, and the statements of Theorem 8 and Lemma 9 contain the slips recorded below. None of these results has a machine-checked proof. The mission produces a checked AIM recursion, a pathwise domination of excess inventory by a queue, and hitting-time and busy-period bounds for random walks with nonnegative i.i.d. decrements.

Difficulty

The argument behind Theorem 2 dominates $y_t-\hat y_t$ by a queue whose inflow $\rho/\sqrt t$ is below the mean demand. For large $\gamma$ the inflow $m/\sqrt t$ exceeds $E[D_1]$ in early periods, so the queue $Z(m)$ is unstable at first and its busy periods are not controlled by a stationary queue. A direct bound on $E[\sum_t Z_t(m)]$ through busy periods of $W(m)$ fails, because $W(m)$ may never empty when $m\ge E[D_1]$ . The proof therefore separates a random initial stretch, which ends at the first time after $\tilde T$ that $Z(m)$ empties, from the remainder. The two parts are bounded by different processes. The random index $\tilde K$ sits inside the sums, so the expectations have to be handled with that dependence.

Formalization scope

Demand uses the published definition CappedBaseStock_Model (DemandLaw, the i.i.d. path measure demandPathLaw). Its law has finite and strictly positive mean. The cost $Q$ and $y^{NV}$ are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. Both are reused, not redefined.
The demand path is zero-based: the paper's $D_t$ is d (t-1). AIM is a deterministic recursion on the path, and $\hat y_t,y_t,x_t$ depend on $D_1,\dots,D_{t-1}$ only. Levels are real numbers, and $Q$ is evaluated at nonnegative levels.
The conventions are $Z_1=W_1=0$ and $\tau_0=1$ . The paper's own indexing ( $Z_0=0$ in (7)) is undefined at $t=0$ , and these are the conventions its proofs use.
$K$ , $|J_1|$ and $\tilde K$ take values in $[0,\infty]$ , and $E[K]$ , $E[|J_1|^2]$ , $E[\tilde K]$ are Lebesgue integrals in $[0,\infty]$ . Theorem 8 and Claim (14) are stated in $[0,\infty]$ . A divergent expectation therefore makes a bound trivially true. It can never make a bound false or vacuous through a junk value $0$ . $\Lambda_2(T)$ is a real expectation of a bounded integrand.
Explicit readings of loose phrases: "for any choice of the parameter $\gamma$ " means every $\gamma>0$ . "Set $y_1=\hat y_1$ to any value in $[0,\bar y]$ " means the statements hold for every such start. "With probability one" in the coupling is stated pathwise. $0<\rho'$ is added (the bound divides by $\rho'$ ), as are $h,b,\bar y>0$ . In Claim (14) the random lower limit $\tilde K$ is read inside the expectation, as in (13) and Appendix E.
Lemma 9 is false as printed: for $D\equiv1$ , $\theta=0$ , $z=1/4$ one has $K=1$ while the printed bound is $1/2$ . The mission states it with an additive $1$ , which is what the printed proof gives once the integers below $2z/(E[D_1]-\theta)$ are counted correctly.
Ruled out: stating the goal about an arbitrary sequence of levels instead of the AIM recursion, taking $E[K]$ or $E[|J_1|^2]$ as real Bochner integrals (which are $0$ when the expectation diverges and would make the bound false), and dropping the newsvendor bound $y^{NV}\le\bar y$ from the goal.
Welcome contributions: a reusable Lindley-recursion (see Asmussen 2003, Ch. III) and busy-period library (the inspection-paradox bound $E|J_{i(\theta,s)}(\theta)|\le E|J_1(\theta)|^2$ , Lemma 13 of the paper), fourth-moment Markov bounds for sums of i.i.d. centred variables, and shift invariance of the i.i.d. path measure.

Selected references

W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1):103–123, 2009. https://doi.org/10.1287/moor.1080.0355
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 2: For g = 0 ≤ f, the Tour ψ′ Minimizes the Largest Changeover CostResearch Paper

Motivation

A machine whose condition is described by one real number — the temperature of a furnace, the setting of a cutting knife — must process $N$ jobs in some order. Job $i$ must be started in state $A_i$ and leaves the machine in state $B_i$ ; moving the state between jobs costs money. Ordering the jobs so that the machine returns to its starting job after the last one is a traveling salesman problem whose distance matrix has a special structure. P. C. Gilmore and R. E. Gomory showed in 1964 (Oper. Res. 12(5), 655–679) that this special traveling salesman problem can be solved exactly with $O(N^2)$ operations, one of the first nontrivial polynomially solvable cases of the problem.

The same paper also treats a second objective: instead of the total changeover cost, minimize the largest single changeover cost of the cycle. This is the bottleneck traveling salesman problem, relevant whenever the binding constraint is the worst transition (a maximal temperature swing, a longest retooling) rather than the total. Without the tour constraint it is the bottleneck assignment problem solved by O. Gross (RAND, 1959). Gilmore and Gomory solve the bottleneck tour problem for the cost matrix of their model when only increases of the state cost anything. This mission formalizes that solution.

Timeline: Gross (1959) solves the bottleneck assignment problem; Gilmore and Gomory (1964) solve the sum and bottleneck traveling salesman problems for one state-variable costs; Gilmore, Lawler and Shmoys survey the well-solved special cases of the traveling salesman problem in The Traveling Salesman Problem (Wiley, 1985), where this case is a standard entry.

Setting

There are $N = n+1$ jobs. Job $i$ has a starting state $A_i\in\mathbb R$ and a final state $B_i\in\mathbb R$ , and the jobs are numbered so that $B_1\le B_2\le\dots\le B_N$ . Given two cost densities $f, g:\mathbb R\to\mathbb R$ , the cost of having job $j$ follow job $i$ is

c_{ij} = \int_{B_i}^{A_j} f(x)\,dx \ \text{ if } A_j\ge B_i,\qquad c_{ij} = \int_{A_j}^{B_i} g(x)\,dx \ \text{ if } B_i > A_j .

A permutation $\psi$ of the jobs means "job $\psi(i)$ follows job $i$ ". It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if $\psi$ is a single cycle. The bottleneck cost of $\psi$ is

m(\psi) = \max_{1\le i\le N} c_{i\psi(i)} .

The bottleneck case of the paper is $g = 0$ and $f\ge 0$ : lowering the state is free, raising it costs $\int f$ .

A permutation $\varphi$ ranks the $A$ 's if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . An interchange $\alpha_{ij}$ is the transposition of $i$ and $j$ ; $\psi\alpha_{ij}$ means "first apply $\alpha_{ij}$ , then $\psi$ ". The graph $G_\varphi$ has the jobs as nodes and an undirected arc $R_{i\varphi(i)}$ for each $i$ ; $R_{q,q+1}$ is the arc joining consecutive nodes $q$ and $q+1$ . A spanning tree of $G_\varphi$ is a set $T$ of arcs $R_{q,q+1}$ such that $G_\varphi\cup T$ is connected and no proper subset of $T$ connects $G_\varphi$ . In the bottleneck case the arc $R_{q,q+1}$ is given the cost $c_{q\varphi(q+1)}$ , and a minimum spanning tree minimizes the sum of these costs. If its arcs are $R_{j_1,j_1+1},\dots,R_{j_m,j_m+1}$ with $j_1<\dots<j_m$ , the paper's candidate tour is

\psi' = \varphi\,\alpha_{j_1 j_1+1}\,\alpha_{j_2 j_2+1}\cdots\alpha_{j_m j_m+1}.

Formalization targets

Goal: $\psi'$ solves the bottleneck traveling salesman problem

For $B$ sorted, $f\ge0$ locally integrable, $g=0$ , $\varphi$ ranking the $A$ 's and $T$ a minimum spanning tree as above,

\psi' \text{ is a tour}\quad\text{and}\quad m(\psi')\le m(\psi)\ \text{ for every tour } \psi .

The goal fixes no numerical constant. It asserts both that the construction produces a tour and that the tour is optimal, so it is a statement about the paper's algorithm, not only about the optimal value.

Milestones

Lemma 8 (p. 668): for a fixed $q$ , the number of $i$ with $i\le q<\varphi^{-1}\psi(i)$ equals the number of $j$ with $\varphi^{-1}\psi(j)\le q<j$ .
Lemma 7 (p. 668): for a tour $\psi$ , the graph $G_\psi^*$ — $G_\varphi$ plus the arcs $R_{q,q+1}$ selected by these two conditions — is connected.
Eq. (30) (p. 670): if $R_{q,q+1}$ is an arc of $G_\psi^*$ not in $G_\varphi$ , then $m(\psi)\ge c_{q\varphi(q+1)}$ .
$\varphi$ minimizes $m$ (p. 671): $m(\varphi)\le m(\psi)$ for every permutation $\psi$ .
The value of $m(\psi')$ (p. 671): $m(\psi')$ equals some $c_{j\varphi(j)}$ or the cost $c_{q\varphi(q+1)}$ of an arc of $T$ .
Theorem 6, corrected (p. 671): for a directed graph with nested out-neighbourhoods $\Gamma_1\subseteq\dots\subseteq\Gamma_N=\{1,\dots,N\}$ and $\varphi$ listing them as initial segments, a Hamiltonian circuit exists iff $\varphi(q)\in\Gamma_q$ for all $q$ and the graph $G'_\varphi$ is connected.

Significance

The result gives an exact solution of a bottleneck traveling salesman problem by one minimum spanning tree computation and a fixed sequence of transpositions. Since general bottleneck traveling salesman problems are NP-hard, cases with an exact algorithm are the reference points against which heuristics and approximation results are compared. Theorem 6, an application, characterizes Hamiltonicity for directed graphs whose out-neighbourhoods form a chain, a class on which the general Hamiltonian circuit problem becomes a connectivity test.

The result is proved in the paper; the mission formalizes the proof. To our knowledge none of it has a machine-checked proof. The formalization adds two things to the paper. First, the statements are made explicit: the order in which interchanges are applied, the reading of "spanning tree", the integrability of $f$ . Second, Theorem 6 as printed is false (see below), and the mission states and asks for a proof of the corrected version. Machine-checked statements of $G_\psi^*$ and Lemmas 7–8 are also the shared core of the companion mission on the minimal sum tour.

Difficulty

The obvious argument — every tour must "cross" each gap between consecutive components of $G_\varphi$ , so it pays at least the cheapest crossing — fails because the cost of a crossing is not intrinsic to the gap: a tour may cross between components using arcs that are not of the form $R_{q,q+1}$ , and $m$ looks at one arc at a time, not at a sum. The connection between an arbitrary tour and the spanning trees of $G_\varphi$ goes through the auxiliary graph $G_\psi^*$ and a counting argument (Lemma 8), and the sum-minimizing tree must be shown to be bottleneck-optimal as well. For the upper bound, the transpositions in $\psi'$ cascade along runs of consecutive tree arcs, so $\psi'(i)$ need not be $\varphi(i)$ or $\varphi(i+1)$ ; only the maximum $m(\psi')$ has that form, and showing it needs the monotonicity of $c_{ij}$ in $A_j$ and $B_i$ , which holds because $f\ge0$ and $g=0$ .

Formalization scope

Jobs are Fin (n + 1) (0-based; the paper's job $i$ is index $i-1$ ). $A, B : \text{Fin}(n+1)\to\mathbb R$ with Monotone B. The cost keeps the general two-density form (1); the bottleneck hypotheses are $f\ge0$ everywhere, $g$ identically $0$ , and $f$ locally integrable, so that every interval integral is genuine. Permutations are Equiv.Perm, and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j. $m$ is a Finset.sup' over all jobs, including those that $\psi'$ leaves unchanged. The arc $R_{q,q+1}$ is indexed by q : Fin n.

Explicit readings of the paper's phrases:

"tour": $\psi(s)\ne s$ for every nonempty proper subset $s$ (the empty set is always fixed);
"a minimal set of additional arcs that connect": a connecting set of arcs $R_{q,q+1}$ none of whose proper subsets connects;
"minimum spanning tree … with these new costs": minimum sum of $c_{q\varphi(q+1)}$ over all such trees, not a bottleneck tree;
" $j_1,\dots,j_m$ in increasing order": the interchanges are applied to $\varphi$ in increasing index, lowest first;
" $\psi'$ minimizes $m(\psi')$ ": $\psi'$ is a tour and $m(\psi')\le m(\psi)$ for every tour $\psi$ ;
Theorem 6: the condition $\varphi(q)\in\Gamma_q$ for all $q$ is added, without which sufficiency fails (for $N=3$ , $\Gamma_1=\Gamma_2=\{3\}$ , $\Gamma_3=\{1,2,3\}$ , $\varphi=(3,1,2)$ , $G'_\varphi$ is connected but no Hamiltonian circuit exists); the existence of $\varphi$ is a hypothesis, not a claim.

Not formalized: the remark that the results hold for $f=0$ , $g\ge0$ ; the remark that $\psi'=\psi^*$ when $B_i\ge A_{\varphi(i)}$ ; the $O(N^2)$ operation count.

Trivializing formalizations are ruled out: with a Bochner integral and no integrability hypothesis every cost could collapse to $0$ and every claim would hold; dropping the tour conjunct of the goal would let $\varphi$ itself be "optimal"; and a maximum that ignored the unchanged arcs $c_{j\varphi(j)}$ would make the goal false.

The traveling salesman items already on the platform (metric and symmetric models with tours as visiting orders, e.g. MetricTSP, TSPHeuristics.Shared.TSPModel) describe a different model and are not used. A complete development needs permutation cycle structure (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, and interval integrals of nonnegative functions; the lemmas on $G_\psi^*$ and Lemma 8 are reusable for the sum objective. Proofs of any milestone are welcome independently.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5) (1964), 655–679. https://doi.org/10.1287/opre.12.5.655
O. Gross, The bottleneck assignment problem, RAND Corporation P-1630, 1959. https://www.rand.org/pubs/papers/P1630.html
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in E. L. Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, 1985, 87–143. ISBN 978-0-471-90413-7

9 thms3 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 3: The Nonquadratic Method of Multipliers for Linear Equality Constraints ConvergesResearch Paper

Motivation

The method of multipliers (augmented Lagrangian method) of Hestenes and Powell is one of the standard algorithms for constrained convex optimization. Each iteration minimizes the Lagrangian plus a quadratic penalty on the constraint residual, then updates the multiplier estimate. Rockafellar showed in 1976 that this method is the proximal point algorithm applied to the dual problem (Rockafellar, Math. Oper. Res. 1976), which explains its global convergence for convex programs without differentiability or constraint qualifications on the primal side.

The quadratic penalty is not the only one used in practice. Exponential and other nonquadratic penalties produce twice-differentiable augmented Lagrangians and were studied by Kort and Bertsekas and by Tseng and Bertsekas. Eckstein (Math. Oper. Res. 18(1), 1993, 202–226) gave a uniform convergence theory for such methods. He replaces the squared Euclidean distance in the proximal point algorithm by the D-function of a Bregman function $h$ , proves convergence of the resulting algorithm for every maximal monotone operator (Theorem 1), and then derives nonquadratic multiplier methods by applying it to the dual of a convex program. This mission covers the linear-equality-constrained case, §4.1 and Theorem 6 of that paper.

Setting

Let $f : \mathbb R^n \to (-\infty, +\infty]$ be convex and lower semicontinuous, let $A$ be an $m \times n$ matrix, $b \in \mathbb R^m$ , and $X \subseteq \mathbb R^n$ closed and convex, with $\inf\{f(x) \mid x \in X\} < \infty$ . The problem is

\text{minimize } f(x) \quad\text{such that}\quad Ax = b,\ x \in X. \tag{7}

Write $\delta_X$ for the indicator function of $X$ ( $0$ on $X$ , $+\infty$ off $X$ ) and $f_X = f + \delta_X$ . The dual functional is

d(p) = \inf_{x \in X}\bigl\{ f(x) + \langle p, Ax - b\rangle \bigr\}, \qquad p \in \mathbb R^m,

assumed not identically $-\infty$ . An optimal multiplier (Lagrange multiplier) is a maximizer of $d$ over $\mathbb R^m$ .

For an open set $S$ , a Bregman function with zone $S$ is a function $h : \bar S \to \mathbb R$ that is continuously differentiable on $S$ , strictly convex and continuous on $\bar S$ , and satisfies the level-set and limit conditions (iv)–(vi) of Definition 1 on its D-function $D_h(x, y) = h(x) - h(y) - \langle \nabla h(y), x - y \rangle$ . Here the zone is all of $\mathbb R^m$ , and $\nabla h$ is assumed onto $\mathbb R^m$ . Let $h^*(z) = \sup_p\{\langle p, z\rangle - h(p)\}$ be the convex conjugate of $h$ , and let $c_k > 0$ with $\inf_k c_k > 0$ . The nonquadratic method of multipliers generates $\{(x^k, p^k)\}$ by

x^{k+1} \in \operatorname*{arg\,min}_{x \in X}\Bigl\{ f(x) + \tfrac{1}{c_k}\, h^*\bigl(\nabla h(p^k) + c_k(Ax - b)\bigr)\Bigr\}, \qquad p^{k+1} = \nabla h^*\bigl(\nabla h(p^k) + c_k(Ax^{k+1} - b)\bigr). \tag{9}

For $h(p) = \frac12\|p\|^2$ this is the classical method of multipliers. A run of the general Bregman proximal point algorithm for an operator $T$ is a sequence with $\frac{1}{c_k}(\nabla h(x^k) - \nabla h(x^{k+1})) \in T(x^{k+1})$ for all $k$ .

Formalization targets

Goal: Theorem 6 (pp. 212–213)

Under the assumptions above:

\exists\, p^\star \text{ optimal} \;\Longrightarrow\; p^k \to \text{some optimal multiplier, and every limit point of } \{x^k\} \text{ solves (7)};

\nexists\, p^\star \text{ optimal} \;\Longrightarrow\; \{p^k\} \text{ is unbounded}.

The statement fixes no penalty: it holds for every Bregman function with zone $\mathbb R^m$ and surjective gradient. It makes no claim that $\{x^k\}$ converges, which is false in general.

Milestones

Theorem 1 (pp. 206–207): for a maximal monotone $T$ and a Bregman function $h$ with zone $S$ , $\bar S \supseteq \operatorname{dom} T$ , a run of the Bregman proximal point algorithm converges to a zero of $T$ when one exists, under either (C1) $S \supseteq \overline{\operatorname{dom} T}$ or (C2) $T = \partial f$ for a closed proper convex $f$ . If $T$ has no zero and (C1) holds, the run is unbounded.
Proof of Theorem 6, p. 213: the multipliers produced by (9) form a Bregman proximal point run on $\partial(-d)$ ,

p^{k+1} = \bigl(\nabla h + c_k \partial(-d)\bigr)^{-1}\bigl(\nabla h(p^k)\bigr).

Proof of Theorem 6, p. 214: if $p^k \to p^\star$ with $p^\star$ optimal, then $Ax^k \to b$ , and every limit point $x^\infty$ of $\{x^k\}$ satisfies $Ax^\infty = b$ , $-A^{\mathsf T}p^\star \in \partial f_X(x^\infty)$ , and solves (7).

An additional item states the existence clause of Theorem 6: if the row space of $A$ meets $\operatorname{ri}(\operatorname{im} \partial(f + \delta_X))$ , or $f$ and $X$ are polyhedral and the row space meets $\operatorname{im} \partial(f + \delta_X)$ , then (9) has an infinite run from every starting point $(x^0, p^0)$ .

Significance

Theorem 6 gives global convergence of a whole family of augmented Lagrangian methods at once, with the penalty chosen through $h$ . For instance, Example 5 of the paper obtains the method with penalty $\frac{1}{r c_k}\sum_i |\mu_i + c_k(A_i x - b_i)|^r$ for any $r > 1$ . Its multiplier sequence behaves exactly as the dual proximal point iterates do, and it detects dual unsolvability through divergence of $\{p^k\}$ . Primal limit points are optimal without any assumption beyond existence of a Lagrange multiplier.

The result has a published proof (Eckstein 1993) but, to our knowledge, no machine-checked proof. Formalizing it requires a formal treatment of Bregman functions and of the Bregman proximal point algorithm (Theorem 1). It also requires the subdifferential calculus of the dual functional: conjugates, the chain rule $\partial(g \circ A^{\mathsf T})$ , and the inverse relation between $\nabla h$ and $\nabla h^*$ . The milestones isolate the reduction of (9) to Theorem 1 and the primal recovery argument, each of which can be proved independently of the others.

Difficulty

The reduction step is where a direct argument fails. Showing that $p^{k+1}$ is a proximal point of $\partial(-d)$ needs the inclusion $-(Ax^{k+1} - b) \in \partial(-d)(p^{k+1})$ , where $-d(p) = (f_X)^*(-A^{\mathsf T}p) + \langle b, p\rangle$ is a composition of a conjugate with a linear map. The subdifferential chain rule holds with equality only under a qualification condition. The argument must therefore use only the inclusion that holds unconditionally, together with the optimality condition for the $x$ -subproblem, which needs differentiability of $h^*$ everywhere (supplied by $\operatorname{im} \nabla h = \mathbb R^m$ and strict convexity of $h$ ). On the primal side, $\{x^k\}$ need not be bounded or convergent, so primal optimality can only be asserted for limit points, through closedness of the graph of $\partial f_X$ . Theorem 1 itself rests on the Bregman conditions (iv)–(vi), which replace the Fejér monotonicity of the Euclidean proximal point argument.

Formalization scope

$\mathbb R^k$ is EuclideanSpace ℝ (Fin k). $A$ is a continuous linear map $\mathbb R^n \to \mathbb R^m$ (equivalent to an $m \times n$ matrix), and $A^{\mathsf T}$ is its adjoint. Theorem 1 is stated on any finite-dimensional real inner product space.
Functions into $(-\infty, +\infty]$ are EReal-valued with "never $-\infty$ " as a hypothesis. $\partial f$ uses the published IsSubgradient; convexity is convexity of the epigraph (IsConvexFn). Maximal monotonicity, dom and zer are the published ThreeOpSplitting.Convergence definitions. The conjugate $h^*$ is the published fenchelConjugate, an EReal supremum.
(9) uses the real value of $h^*$ . This is faithful because $\operatorname{im}\nabla h = \mathbb R^m$ makes $h^*$ finite everywhere. Finiteness of $h^*$ is a consequence, never a hypothesis. The arg min in (9) is a minimality predicate, not a choice function, since the minimizer need not be unique.
Recursion (3) is encoded through its equivalent form (4). Condition (vi) of Definition 1 is stated on the natural domain $\bar S \times S$ of $D_h$ .
"Limit point" means subsequential limit, and "unbounded" means the range of the sequence is not bounded. In the existence clause, ri is Mathlib's intrinsicInterior, and polyhedral sets and functions are finite intersections of closed half-spaces (for functions, of the epigraph).
The paper's typo "monontone" in Theorem 1 is read as "monotone".
The convergence claims must not be weakened to their trivial instances. A formalization that assumes $\{x^k\}$ converges, or adds finiteness of $h^*$ or boundedness of $\{p^k\}$ as a hypothesis, or encodes (9) with a choice function, does not state Theorem 6.
Reusable beyond this mission: the Bregman function structure and Theorem 1 (shared with the other missions of this series), and the dual-functional and conjugate facts for linearly constrained programs. Contributions toward the conjugate calculus ( $\nabla h^* = (\nabla h)^{-1}$ , the chain rule inclusion) are welcome.

Selected references

J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1) (1993) 202–226. https://doi.org/10.1287/moor.18.1.202
R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2) (1976) 97–116. https://doi.org/10.1287/moor.1.2.97
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
Y. Censor, S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3) (1992) 451–464. https://doi.org/10.1007/BF00940051
P. Tseng, D. P. Bertsekas, On the convergence of the exponential multiplier method for convex programming, Mathematical Programming 60 (1993) 1–19. https://doi.org/10.1007/BF01580598

9 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 3: With One Markdown or Markup Allowed, Thresholds x_n < z_n Give the Optimal PolicyResearch Paper

Motivation

Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.

Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).

Setting

There are three prices $p_1 < p < p_2$ . At price $p_i$ demand is a Poisson process of intensity $\lambda_i$ , and at $p$ of intensity $\lambda$ , with

\lambda_1 > \lambda > \lambda_2, \qquad r_1 > r > r_2, \qquad r_i = p_i\lambda_i,\ r = p\lambda,

all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section $p_1$ is the lower price; the initial price is $p$ .

A seller with $n$ units and time-to-go $t$ sells at $p$ and may switch once, to $p_1$ or to $p_2$ . Write $N(\cdot)$ for the demand process at $p$ and $N_i(\cdot)$ for that at $p_i$ .

$J^i(n,t;s) = (p - p_i)E\min(n,N(s)) + p_iE\min(n, N(s) + N_i(t-s))$ is the expected revenue of switching to $p_i$ after $s$ time units.
$J(n,t;0) = \max\{J^1(n,t;0), J^2(n,t;0)\}$ is the revenue of switching at once to the better alternative, and $J(n,t;t) = pE\min(n,N(t))$ the revenue of never switching.
The optimal revenue is

J(n,t) = \sup_{\tau \in \mathcal T} E\bigl[p\min(n,N(\tau)) + J(n - N(\tau), t - \tau; 0)\bigr],

where $\mathcal T$ is the set of stopping times of the history of $N$ with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.

$G^i(n,t) = r - r_i - p_i(\lambda - \lambda_i)P(N_i(t) \ge n)$ .
$\Delta^i(n,t) = J(n,t;t) - J^i(n,t;0)$ and $\Delta(n,t) = J^1(n,t;0) - J^2(n,t;0)$ , with first positive zeros $t^i_n$ and $t_n$ .

Formalization targets

Goal: Theorem 3 (pp. 1385–1386)

Under the paper's assumption $t^1_n < t_n < t^2_n$ for every $n$ , there are strictly increasing sequences $(x_n)$ , $(z_n)$ with

x_n < t^1_n < t_n < t^2_n < z_n

such that $J(n,t) = V(n,t)$ , where $V(n,t) = J(n,t;0) + F(n,t)$ for $x_n \le t \le z_n$ and $V(n,t) = J(n,t;0)$ otherwise. The excess $F(n,\cdot)$ equals $H^1(n,\cdot)$ on $[x_n,t_n]$ and $H^2(n,\cdot)$ on $[t_n,z_n]$ . Each $H^i$ solves

\frac{\partial H}{\partial t} = -\lambda H + L^i(n,t), \qquad L^i(n,t) = G^i(n,t) + \lambda\bigl[V(n-1,t) - J^i(n-1,t;0)\bigr],

with $H^1(n,x_n) = 0$ and $H^2(n,t_n) = H^1(n,t_n)$ . The thresholds are $x_n = \inf\{t \ge 0 : L^1(n,t) = 0\}$ and $z_n = \inf\{t \ge t_n : H^2(n,t) \le 0\}$ .

Milestones

(16), p. 1385: $\partial J^i(n,t;0)/\partial t = r - \lambda[J^i(n,t;0) - J^i(n-1,t;0)] - G^i(n,t)$ .
Lemma 2, p. 1379, in both cases: the zeros of $G(n,\cdot)$ increase strictly in $n$ , and $G(n,\cdot)$ changes sign exactly once.
Lemma 3, p. 1382, in both cases: $J(n,t;t) - J(n,t;0)$ changes sign exactly once at a strictly increasing sequence $t_n$ , and is monotone beyond it.
Lemma 1, p. 1378: a verification criterion identifying $J(n,t)$ as the solution of a system of differential equations and inequalities.

Significance

Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With $m$ units left and time-to-go $u$ , the seller marks down at once when $u$ falls below $x_m$ , marks up at once when $u$ exceeds $z_m$ , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of $2n$ numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.

Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.

Difficulty

The value $J(n,t)$ is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock $n+1$ are defined through $V(n,\cdot)$ , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that $L^1(n+1,\cdot)$ again has a single sign change, which requires $V(n,\cdot) - J^1(n,\cdot;0)$ to be increasing beyond $x_n$ . One must also know that $H^2(n+1,\cdot)$ is positive up to $t^2_{n+1}$ and eventually negative, so that $z_{n+1}$ is finite, and that $z_n < z_{n+1}$ . These facts concern three different price pairs at once: $(p,p_1)$ , $(p,p_2)$ and $(p_1,p_2)$ . A direct comparison of $V$ with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on $V$ matters.

Formalization scope

Model. Demand at $p$ is the counting process of i.i.d. exponential interarrival times from the published definition QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and $N_i(t-s)$ enters only through its law: the sum $N(s) + N_i(t-s)$ is written through its Poisson $(\lambda s + \lambda_i(t-s))$ law. $\mathcal T$ is the class of real-valued stopping times $\tau$ of the σ-algebras generated by the counts $N(u)$ , $0 \le u \le s$ , with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.
Conventions. Time is time-to-go, $t \ge 0$ ; ODEs are imposed at every $t > 0$ through HasDerivAt. Threshold sequences are indexed from $n = 1$ . Every infimum is a real sInf paired with the nonemptiness of its set. $F$ , $H^1$ , $H^2$ , $V$ and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption $t^1_n < t_n < t^2_n$ is a hypothesis of the goal, as on the page.
Added hypotheses. Prices and intensities are positive, the paper's standing convention. Lemma 1 as printed is false. It is stated with the boundary condition $V(n,0) = J(n,0;0)$ , the zero-stock condition $V(0,t) = 0$ , the obstacle condition $V \ge J(\cdot;0)$ , and local Lipschitz continuity of $V$ in place of "continuous and almost everywhere differentiable". The page's proof uses all four. Lemma 2's printed "bounded" is corrected to "bounded away from zero", since $y_n \to \infty$ .
No trivialization. No statement assumes the optimality identity, the verification conditions, the derivative identity (16), or any sign-change fact as a hypothesis. A goal that defined $V$ and assumed $J = V$ , or that left the thresholds unrelated to $L^1$ and $H^2$ , would not be Theorem 3.
Infrastructure needed. Poisson tail calculus (differentiation of $E\min(n, N(t))$ in $t$ ), variation-diminishing properties of the kernel $e^{-\lambda(t-u)}$ , linear first-order ODEs, and a martingale decomposition for Poisson counting processes evaluated at bounded stopping times. Contributions of any of these, or of proofs of the milestones, are welcome.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8):1371–1391, 1995. https://doi.org/10.1287/mnsc.41.8.1371
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
S. Karlin, Total Positivity, Vol. 1, Stanford University Press, 1968.
G. Bitran and R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003. https://doi.org/10.1287/msom.5.3.203.16031

10 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 2: Markup Is Optimal Once Time-to-Go Exceeds an Increasing Threshold z_nResearch Paper

Why a promotional fare needs a switching rule

An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.

The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.

Demand, inventory, and admissible decisions

There are $n\ge1$ items and $t\ge0$ units of time-to-go. At price $p_i$ , sales requests follow a Poisson counting process $N_i$ with rate $\lambda_i$ . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has

0<p_1<p_2,\qquad 0<\lambda_2<\lambda_1,\qquad p_2\lambda_2<p_1\lambda_1.

The salvage value at the end of the horizon is zero. A fixed switch at time $s\in[0,t]$ charges $p_1$ first and $p_2$ afterwards. Its expected revenue, denoted $J(n,t;s)$ , is

J(n,t;s)=(p_1-p_2)\sum_{j=1}^n\Pr\{N_1(s)\ge j\} +p_2\sum_{j=1}^n\Pr\{N_1(s)+N_2(t-s)\ge j\}.

The two counts in the last term are independent, so their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . This is the expression in §3 of the paper. In particular, $J(n,t;0)$ is the revenue from increasing the price immediately.

An admissible switching time $\tau$ uses only the history of sales at $p_1$ ; it lies between zero and $t$ and cannot wait past stock exhaustion. The optimal value $J(n,t)$ is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.

Formalization targets

The goal is Theorem 2 on pp. 1382–1383. Define the switching function

G(n,t)=p_1\lambda_1-p_2\lambda_2 -p_2(\lambda_1-\lambda_2)\Pr\{N_2(t)\ge n\}, \qquad y_n=\inf\{u\ge0:G(n,u)=0\}.

There are thresholds $x_n,z_n$ with $y_n\le x_n<z_n$ , and $(z_n)_{n\ge1}$ is increasing. A continuation premium $F$ gives the value

J(n,t)=\begin{cases} J(n,t;0)+F(n,t),&t<z_n,\\ J(n,t;0),&t\ge z_n. \end{cases}

For $n\ge1$ , $F(n,t)=H(n,t)$ below $z_n$ and is zero at or above it; $F(0,t)=0$ . The function $H$ satisfies $H(n,0)=0$ and the differential equation $\partial_tH(n,t)=-\lambda_1H(n,t)+L(n,t)$ , where $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ . The remaining thresholds are the first nonnegative zero of $L(n,\cdot)$ and the first positive zero of $H(n,\cdot)$ :

x_n=\inf\{u\ge0:L(n,u)=0\},\qquad z_n=\inf\{u>0:H(n,u)=0\}.

The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of $G$ , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.

What the result supplies

The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for $z_n$ : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for $F$ and $H$ , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.

Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.

Where the difficulty lies

The immediate-switch comparison $G(n,t)$ has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For $n>1$ , the relevant forcing term is $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , so the sign of $G$ alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.

Formalization scope

The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as $\min(n,N_1(\tau))$ , equal almost surely to $N_1(\tau)$ for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.

Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for $y_n$ , $x_n$ , and $z_n$ is nonempty; it also keeps $u>0$ in the definition of $z_n$ , since $H(n,0)=0$ . Continuity of $H(n,\cdot)$ at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; $y_n$ is unbounded as stock grows. These choices are recorded for review in the moderation notes.

The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Convex Optimization Information Theory Probability+1·Captain: mikedeng1

I-Divergence Geometry of Probability Distributions and Minimization Problems 2: Under Moment Constraints the I-Projection Exists at Every Interior Point and Has Exponential-Family DensityResearch Paper

Minimum discrimination information under moment constraints

Given a reference probability distribution $R$ and a set $\mathcal E$ of probability distributions, the minimum discrimination information problem asks for the member of $\mathcal E$ closest to $R$ in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations $\int f_i\,dP = a_i$ , and the classical answer is that the minimizer is an exponential family member, with density $c\exp\sum_i t_i f_i$ with respect to $R$ .

That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the $f_i$ .

Timeline:

1959: Kullback formulates the minimum discrimination information theorem: an element of $\mathcal E$ of exponential form is the minimizer (a sufficient condition).
1966: Kullback and Khairat (Ann. Math. Statist. 37, 1966) refine the sufficient condition.
1972: Čencov proves existence of exponential-form minimizers under general conditions (Statistical Decision Rules and Optimal Inference, Theorem 23.1).
1975: Csiszár proves Theorem 3.3 by the minimizing-sequence method of his Theorem 2.1; a first version of the paper assumed $T_R = E^k$ , weakened to " $T_R$ open" after Čencov's work.

Setting

All distributions (PD's) live on one measurable space $(X,\mathcal X)$ . The I-divergence of $P$ from $Q$ is

I(P\|Q)=\int \log p_Q\,dP\ \text{ if } P\ll Q,\qquad I(P\|Q)=+\infty\ \text{ otherwise},

where $p_Q$ is the density of $P$ with respect to $Q$ ; it takes values in $[0,\infty]$ and vanishes only for $P=Q$ . The variation distance is $|P-Q|=\int|p_R-q_R|\,dR$ for any PD $R$ dominating both. If $\mathcal E$ is a convex set of PD's containing some $P$ with $I(P\|R)<\infty$ , a $Q\in\mathcal E$ with

I(Q\|R)=\min_{P\in\mathcal E} I(P\|R)

is the I-projection of $R$ on $\mathcal E$ .

Fix real-valued measurable functions $f_1,\dots,f_k$ on $X$ . For $a=(a_1,\dots,a_k)\in E^k$ (Euclidean $k$ -space) the moment set $\mathcal E(a)$ is the set of PD's $P$ with $\int f_i\,dP=a_i$ , $i=1,\dots,k$ . Further:

$A_R$ is the set of $a\in E^k$ for which $\mathcal E(a)$ contains some $P$ with $I(P\|R)<\infty$ ;
$T_R=\{t\in E^k:\ \exp\sum_i t_i f_i \text{ is } R\text{-integrable}\}$ , (3.16);
$F(a)=\inf_{P\in\mathcal E(a)} I(P\|R)$ , (3.18), the optimal value as a function of the constraint levels.

Formalization targets

Goal: Theorem 3.3

If $T_R$ is open in $E^k$ , then for every point $a$ of the interior of $A_R$ the I-projection $Q$ of $R$ on $\mathcal E(a)$ exists and

q_R(x)=c\exp\sum_{i=1}^k t_i f_i(x)\qquad R\text{-a.e.},

for some constant $c$ and some $t\in E^k$ .

Milestones

(2.2), the parallelogram identity: $I(P_m\|R)+I(P_n\|R)=2I(\tfrac{P_m+P_n}2\|R)+I(P_m\|\tfrac{P_m+P_n}2)+I(P_n\|\tfrac{P_m+P_n}2)$ .
(2.4): a minimizing sequence $P_n$ in a convex set converges in variation to a PD $Q\ll R$ (closedness of the set is not used).
Lemma 3.1: if $e^{tf}$ is $Q$ -integrable for small $|t|$ , then $I(P_n\|Q)\to0$ implies $\int f\,dP_n\to\int f\,dQ$ .
(3.18): $A_R$ is convex and $F$ is finite and convex on $A_R$ .
(3.19): at an interior point $a$ of $A_R$ there is $t$ with $F(b)\ge F(a)+\sum_i t_i(b_i-a_i)$ for all $b\in A_R$ .
Remark, p. 158: $F$ is differentiable at interior points of $A_R$ , and $\operatorname{grad}F(a)=t$ , the parameter vector of the I-projection.

Significance

Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.

The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).

Difficulty

The obvious argument fails at the first step: the moment set $\mathcal E(a)$ is convex but not closed in variation when the $f_i$ are unbounded, since $\int f_i\,dP$ is not continuous in variation. A minimizing sequence therefore converges in variation to some $Q$ (as in Theorem 2.1), but nothing places $Q$ in $\mathcal E(a)$ : mass can escape to where $|f_i|$ is large. Ruling this out needs quantitative control of $I(P_n\|Q)$ , which in turn requires knowing the form of $Q$ before knowing $Q$ is feasible; the interplay with the convexity of $F$ and the openness of $T_R$ is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.

Formalization scope

Probability distributions are Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions $\log 0=-\infty$ , $\log\frac a0=+\infty$ , $0\cdot(\pm\infty)=0$ .
The variation distance uses $P+Q$ as dominating measure (the page allows any dominating PD; the value is the same).
The I-projection carries $I(Q\|R)<\infty$ explicitly: the page defines it only when $\mathcal E$ meets $\{P: I(P\|R)<\infty\}$ .
$\mathcal E(a)$ requires $P$ -integrability of every $f_i$ , so the constraint integrals are genuine. $E^k$ is Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. $k=0$ is allowed.
$F$ is an infimum in $[0,\infty]$ (equal to $\infty$ outside $A_R$ ); statements use its real value only on $A_R$ , where it is finite. (3.18) prints $I(P\|Q)$ ; the reference measure is $R$ , as the definition of $A_R$ and the proof show. (3.16) prints $(t_1,\dots,t_n)$ for $(t_1,\dots,t_k)$ .
Densities are Radon–Nikodym derivatives and the form (3.2) is an $R$ -almost-everywhere identity with no exceptional set of positive measure.
Lemma 3.1 asserts that $f$ is $P_n$ -integrable for large $n$ as well as the convergence, so that $\int f\,dP_n$ is not a default value.
Trivializing readings are excluded: the goal asserts existence of the I-projection rather than assuming it, $T_R$ is an integrability set (not a set where a junk integral is finite), and the infimum is never a real sInf over a possibly empty set.

A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) $I(P\|R)-I(P\|Q)=\int\log q_R\,dP$ ), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.

Selected references

I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3(1), 146–158, 1975. https://doi.org/10.1214/aop/1176996454
S. Kullback, Information Theory and Statistics, Wiley, 1959.
S. Kullback and M. A. Khairat, A note on minimum discrimination information, Ann. Math. Statist. 37, 279–280, 1966.
E. T. Jaynes, Information theory and statistical mechanics, Phys. Rev. 106, 620–630, 1957. https://doi.org/10.1103/PhysRev.106.620
N. N. Čencov, Statistical Decision Rules and Optimal Inference (Russian), Nauka, 1972; English translation, American Mathematical Society, 1982.
I. N. Sanov, On the probability of large deviations of random variables (Russian), Mat. Sbornik 42, 11–44, 1957.

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments IV: Uniform Pricing Earns OPT/(1 + ln(v_m/v_1)) in Unit-Demand Min-PricingResearch Paper

Pricing with unit-demand consumers

A seller with $n$ distinct items faces $m$ consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price $q$ on every item and choose $q$ to maximise revenue.

Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a $1/(1+\ln m)$ fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).

Setting

Unit-demand min-pricing ( $\mathrm{UDP}_{\min}$ ). There are items $[n]$ and consumers $[m]$ , $m\ge 1$ . Consumer $i$ is interested in a set $B_i\subseteq[n]$ and has a valuation $v_i>0$ . Given a price assignment $p:[n]\to\mathbb R_{>0}$ , consumer $i$ buys a cheapest item of $B_i$ if its price is at most $v_i$ , and nothing otherwise. The seller's revenue is

\mathrm{rev}_{\mathrm{UDP}}(p)=\sum_{i:\ B_i\ne\emptyset,\ \min_{x\in B_i}p(x)\le v_i}\ \min_{x\in B_i}p(x),

the optimum is $\mathrm{OPT}_{\mathrm{UDP}}=\sup_{p>0}\mathrm{rev}_{\mathrm{UDP}}(p)$ , and uniform pricing earns $\mathrm{UP}=\sup_{q>0}\mathrm{rev}_{\mathrm{UDP}}(q,\dots,q)$ . Write $v_{\max}=v_m$ and $v_{\min}=v_1$ for the extreme valuations.

Regular choice models. A finite product set $\mathcal C$ carries choice probabilities $\mathcal P(x,S)$ for $x\in\mathcal C$ , $S\subseteq\mathcal C$ , with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ . The model is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$ , (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$ , and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$ . With revenues $r:\mathcal C\to\mathbb R_{>0}$ , an assortment earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$ . If $r_1<\dots<r_k$ are the distinct revenues and $S_i=\{x: r(x)\ge r_i\}$ , revenue-ordered assortments earn $\mathrm{RO}=\max_i\mathrm{rev}(S_i)$ .

The reduction. From a $\mathrm{UDP}_{\min}$ instance the paper builds $\mathcal C=[n]\times\{v_1,\dots,v_m\}$ , $r((x,v))=m\,v$ , and $\mathcal P=\frac1m\sum_i\mathcal P_i$ , where $\mathcal P_i$ spreads probability one over the set $Q_i(S)$ of pairs $(x,v)\in S$ with $x\in B_i$ , $v\le v_i$ and $v$ minimal among the pairs of $S$ whose item lies in $B_i$ .

Formalization targets

Goal: Corollary 4.7

\mathrm{OPT}_{\mathrm{UDP}}\ \le\ \Big(1+\ln\frac{v_{\max}}{v_{\min}}\Big)\cdot\mathrm{UP}.

The bound is the paper's "approximates the optimum revenue to within a factor of $1/(1+\ln\rho)$ , $\rho:=v_m/v_1$ ", stated in product form.

Milestones

Lemma 4.5. Some optimal price assignment takes only valuations as prices; in particular $\mathrm{OPT}_{\mathrm{UDP}}$ is attained.
Regularity of the reduction's choice model (proof of Theorem 4.6, pp. 17–18).
Assortments to prices: $\mathrm{rev}(S)=\mathrm{rev}_{\mathrm{UDP}}(p_S)$ with $p_S(x)=\min\{v:(x,v)\in S\}$ (p. 19).
Prices to assortments: for valuation-valued $p$ , $\mathrm{rev}(S_p)=\mathrm{rev}_{\mathrm{UDP}}(p)$ with $S_p=\{(x,v): v\ge p(x)\}$ (p. 19).
Theorem 4.6 for the explicit instance: regularity, positive revenues, equal optima, and the two-way correspondence between threshold sets and uniform valuation prices.
Theorem 3.2 for an arbitrary regular model:

\mathrm{OPT}\le\Big(\sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\Big)\mathrm{RO},\qquad \sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\le 1+\ln\frac{r_k}{r_1},\qquad r_0:=0.

Significance

The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor $\rho$ of each other, a single price recovers a $1/(1+\ln\rho)$ fraction of the optimum, which improves on $1/(1+\ln m)$ whenever $\rho<m$ . More broadly, Theorem 4.6 places $\mathrm{UDP}_{\min}$ inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.

All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no $\mathrm{UDP}_{\min}$ problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.

Difficulty

The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make $Q_i$ nonempty, never empty, and this must be checked for the specific sets $Q_i(S)$ whose definition depends on the whole of $S$ . The revenue identities require tracking the minimum over $B_i$ of a price function obtained from an assortment, including items absent from $S$ , which receive the paper's " $+\infty$ " price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.

The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of $v_m/v_1$ ; the reduction to a regular model is what supplies it.

Formalization scope

Items and consumers are finite types X and M, with Nonempty M ( $m\ge1$ ). Valuations satisfy $v_i>0$ as a field of the instance; the paper says "non-negative", but its reduction ( $r=m\,v>0$ ) and its ratio $v_m/v_1$ need positivity.
A consumer with $B_i=\emptyset$ pays $0$ . Ties among cheapest items do not affect payments, so payments are defined directly.
$\mathrm{OPT}_{\mathrm{UDP}}$ and $\mathrm{UP}$ are real suprema over positive price assignments and positive uniform prices; both index sets are nonempty and the revenues are bounded by $\sum_i v_i$ . Uniform pricing ranges over all $q>0$ , not only valuations.
The no-purchase option is not a product: it is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ , and regularity includes axiom (iv) for it. OPT is a maximum over all Finset C; RO is a maximum over the $k$ threshold sets only. Distinct revenues are sorted 0-based (Fin k), with $r_0=0$ handled as a separate case.
The paper's $+\infty$ price for $p_S$ is the real $1+\sum_i v_i$ , which exceeds every valuation, as its Remark on p. 18 allows. The valuation set collapses equal valuations.
Approximation factors are in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$ ; $\ln$ is Real.log applied to ratios $\ge1$ .
Trivializing readings are excluded: Theorem 4.6 is stated for the explicit instance of its proof, not as the bare existence of a regular instance with the same optimum (a single product of revenue $\mathrm{OPT}_{\mathrm{UDP}}$ would satisfy that); $\mathrm{OPT}_{\mathrm{UDP}}$ ranges over all positive price assignments, not uniform ones; valuations are positive, so no logarithm takes a junk value.
Theorem 3.2 is restated here for this mission's copy of the regular model; it is also the goal of mission I of this series. Reusable pieces: the regular choice model and revenue-ordered value, and the $\mathrm{UDP}_{\min}$ model. Contributions of any milestone, and alternative proofs of Lemma 4.5, are welcome.

Selected references

G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82 (2020). https://arxiv.org/abs/1606.01371
G. Aggarwal, T. Feder, R. Motwani and A. Zhu, Algorithms for multi-product pricing, ICALP 2004. https://doi.org/10.1007/978-3-540-27836-8_8
V. Guruswami, J. D. Hartline, A. R. Karlin, D. Kempe, C. Kenyon and F. McSherry, On profit-maximizing envy-free pricing, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070598
P. Rusmevichientong, B. Van Roy and P. W. Glynn, A nonparametric approach to multiproduct pricing, Operations Research 54(1), 2006. https://doi.org/10.1287/opre.1050.0236
A. Aouad, V. Farias, R. Levi and D. Segev, The approximability of assortment optimization under ranking preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1754

13 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Inventory Control and Price Theory 2: For Style Goods with Uniform Demand Linear in Unit Profit, Expected Profit Is Maximized at P* = ((P₀ − 3L) + √((3L − P₀)² + 16P₀L))/4Research Paper

Pricing and stocking a perishable good

A retailer of style goods — seasonal clothing, newspapers, anything that loses most of its value when the selling period ends — must decide before the season how many units to stock, knowing demand only as a probability distribution. Units left over are liquidated at a loss; units short are sales forgone. This single-period trade-off is the newsvendor problem, and its solution, the critical-fractile rule, is one of the first results of stochastic inventory theory.

In practice the retailer also sets the price, and the price moves the demand distribution. T. M. Whitin's 1955 paper Inventory Control and Price Theory (DOI 10.1287/mnsc.2.1.61) is one of the first to put the two decisions into one model. Its Section 3 restates the critical fractile for a given price, then lets the demand distribution depend on the unit profit and asks for the unit profit and stock that jointly maximize expected profit. For one explicit family of demand laws it solves the problem in closed form. This joint price-setting newsvendor problem later grew into a large literature (Mills 1959, Karlin and Carr 1962, and the survey of Petruzzi and Dada 1999), which cites Whitin's model as its starting point.

Setting

There is one selling period. Stock $x \ge 0$ is on hand at its start. Each unit sold earns the unit profit $P$ ; each unit left over at the close is liquidated at the unit liquidation loss $L > 0$ .

Demand depends on the unit profit through its mean. The mean demand is the linear function

\mu(P) = k\,(P - P_0),

where $P_0 > 0$ is the unit profit at which demand falls to zero and $k$ is the reciprocal of the slope of the line relating unit profit and amount demanded. Demand decreases in $P$ , so $k < 0$ , and the admissible unit profits are $0 < P < P_0$ . At unit profit $P$ , demand $X$ has the rectangular (uniform) distribution on $[0, 2\mu(P)]$ .

The expected marginal profit of the $x$ -th unit is $f(x) = P\,\Pr(X \ge x)$ , the probability that it sells weighted by the unit profit, and the expected marginal loss is $g(x) = L\,\Pr(X < x)$ , the probability that it does not sell weighted by the liquidation loss. The expected profit of stocking $x$ units at unit profit $P$ is the area between them,

E(P, x) = \int_0^x \big[f(t) - g(t)\big]\,dt,

which is the expected profit on sales minus the expected liquidation loss. The equilibrium stock is

x_M(P) = -\frac{2kP(P_0 - P)}{P + L}.

Formalization targets

Goal: the optimal unit profit (Eq. (16))

With

P^* = \frac{(P_0 - 3L) + \sqrt{(3L - P_0)^2 + 16P_0L}}{4},

one has $0 < P^* < P_0$ , and for all $0 < P < P_0$ and all $x \ge 0$

E(P, x) \le E\big(P^*, x_M(P^*)\big),

with equality only at $(P, x) = (P^*, x_M(P^*))$ . The formula for $P^*$ involves only $P_0$ and $L$ : the optimal unit profit is independent of the demand slope $k$ .

Milestones, in the order of the paper

Eq. (8) — for a general demand law, profit is maximized at the stock whose probability of being sold is $L/(G + P + L)$ ( $G$ a goodwill loss per unit short). This is already proved on the platform as SupplyChainTheory.chain_optimal_fractile and enters as a reference.
Eq. (11) — on $0 \le x \le 2\mu(P)$ , $f(x) = \frac{P}{2k(P_0 - P)}x + P$ and $g(x) = \frac{-L}{2k(P_0 - P)}x$ .
Eqs. (10), (13) — on the same range, $E(P, x) = \frac{P + L}{4k(P_0 - P)}x^2 + Px$ .
Eqs. (9), (12) — $x_M(P)$ lies in $(0, 2\mu(P))$ , is the only stock with $f = g$ , and is the unique maximizer of $E(P, \cdot)$ over $x \ge 0$ .
Eq. (14) — $E(P, x_M(P)) = -kP^2(P_0 - P)/(P + L)$ .
Eq. (15) — the derivative of $P \mapsto E(P, x_M(P))$ vanishes exactly when $2P^2 + (3L - P_0)P - 2P_0L = 0$ .
Footnote 7 — the elasticity of mean demand at $P^*$ equals $P^*/(P_0 - P^*)$ , and it tends to $1$ as $P_0 \to \infty$ with $L$ fixed.

Significance

The goal is a complete closed-form solution of a joint pricing-and-stocking problem under uncertainty: one price and one stock level, explicitly, with a proof that no other pair does as well. The independence of the optimal unit profit from $k$ says that, in this family, the scale of the market does not affect the optimal margin; only the ratio of the zero-demand margin to the liquidation loss does. Footnote 7 relates the optimum to the classical monopoly rule (unit elasticity) in the limit of a negligible liquidation loss.

Whitin's derivation is calculus on closed forms and was never stated as a theorem with hypotheses. He calls the stationary point of (15) "the optimal $P$ " without checking that it is a maximum, that it is global, or that the stock beyond the support of demand cannot do better. The formalization fixes all three: the goal is a statement of global, unique optimality over the whole admissible region. No machine-checked proof of this result, of the price-setting newsvendor, or of the uniform-demand newsvendor exists on the platform; the general critical-fractile rule (8) is the only part of Section 3 already proved there.

Difficulty

The expected profit is defined from the demand law, so the closed forms (11) and (13) must be derived from the uniform distribution — probabilities of half-lines under a conditioned Lebesgue measure, and an interval integral of the resulting piecewise-linear functions. They hold only on the support of demand; beyond $2\mu(P)$ the marginal profit is $0$ and the marginal loss is $L$ , and the global statement must cover that region too.

The pricing step is where the paper is loose. Setting the derivative of (14) to zero gives a quadratic with two real roots, and a stationary point of a function on an open interval need not be its maximum. The goal asks for the global maximum over $0 < P < P_0$ and its uniqueness, and asks that it be the global maximum of the joint problem, not only of the reduced function $P \mapsto E(P, x_M(P))$ .

Formalization scope

All quantities are real numbers; stock is continuous, as in the paper's calculus. Mean demand is meanDemand k P₀ P = k * (P - P₀) and the paper's sign convention is kept: $k < 0$ is a hypothesis of every statement, as are $L > 0$ and $0 < P < P_0$ (or $P_0 > 0$ where $P$ is not fixed). The demand law is ProbabilityTheory.cond volume (Set.Icc 0 (2 * μ)); $f$ and $g$ use $\Pr(X \ge x)$ and $\Pr(X < x)$ ; $E$ is an interval integral defined for every $x$ .

The paper's loose phrases are read as follows. "Equation (9) may be solved for $x$ " becomes uniqueness of the root of $f - g$ on $x \ge 0$ ; "the equilibrium value of $x$ " becomes the unique maximizer of $E(P, \cdot)$ over $x \ge 0$ ; "differentiating (14)" becomes a HasDerivAt statement with the explicit derivative for $P \mapsto E(P, x_M(P))$ , together with the equivalence with (15); "solving (15) gives the optimal $P$ " becomes the goal's joint global maximum with equality case; "independent of $k$ " is the shape of the formula for $P^*$ ; "as $P_0$ becomes large relative to $L$ , the optimal elasticity approaches unity" becomes a limit as $P_0 \to \infty$ with $L$ fixed.

Defining $E$ by the closed form (13) instead of from the demand law would make milestones (11) and (13) tautologies and would change the model beyond the support of demand; this formalization rules that out. The paper's goodwill loss $G$ belongs to the fixed-price model of (8) and does not appear in $E$ .

A complete development needs the uniform distribution's tail probabilities, interval integrals of piecewise-linear functions, and one-variable calculus for the quadratic and the cubic $P^2(P_0 - P)/(P + L)$ ; the uniform-law lemmas are reusable for any newsvendor problem with uniform demand. Proofs of the milestones, and alternative arguments for the goal, are welcome.

Selected references

T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 61–68, 1955. https://doi.org/10.1287/mnsc.2.1.61
E. S. Mills, Uncertainty and Price Theory, Quarterly Journal of Economics 73(1), 116–130, 1959. https://doi.org/10.2307/1883828
S. Karlin and C. R. Carr, Prices and Optimal Inventory Policy, in Arrow, Karlin and Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 159–172, 1962.
N. C. Petruzzi and M. Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 183–194, 1999. https://doi.org/10.1287/opre.47.2.183
L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Eq. (14.8) (the critical fractile, formalized on the platform as SupplyChainTheory.chain_optimal_fractile).

9 thms3 active usersReviewed

Completed

Analysis Operations Research·Captain: mikedeng1

Inventory Control and Price Theory 1: With Linear Demand and Economic Lot Sizes, the Profit-Maximizing Price Satisfies the Cubic (7)Research Paper

Motivation

Inventory calculations often take the selling price as fixed, while price calculations often treat the cost of supplying demand as independent of the order policy. Whitin's 1955 model connects the two decisions in one annual-profit calculation. A merchant chooses both the price charged to customers and the size of each replenishment order. Changing the price changes annual demand; changing demand changes the number of orders, inventory carrying cost, and therefore the economic lot size. This makes the selling price and the inventory decision parts of the same optimization problem. Whitin's paper gives a compact example in which the connection can be written down explicitly.

The mission concentrates on Section 2, the stationary-demand model for a stable item. Section 3 of the paper studies style goods under uncertain sales and belongs to a separate mission. The result here concerns a deterministic annual demand curve and continuous order quantities, so a solver can focus on the interaction between a classical economic order quantity calculation and a price first-order condition.

Setting

The price is a real number $p$ . Annual demand is the linear function $D(p)=ap+b$ , where $a$ and $b$ are given real constants. A feasible price has $D(p)>0$ . The paper does not require $a<0$ in its displayed model, so the formal statements leave the slope unrestricted. Negative $a$ is the economically usual decreasing-demand case; in other regimes a joint maximum may simply fail to exist.

The merchant pays a fixed setup cost $S$ whenever an order is placed. The purchase cost per unit is $C$ , and the annual carrying charge for one unit kept in stock is $IC$ , where $I$ is a carrying-rate factor. If $Q>0$ units are ordered each time, average stock is $Q/2$ and the annual number of orders is $D/Q$ . A per-unit operating cost $k$ is incurred on annual demand, and $f$ is an annual fixed cost. The resulting total variable cost and two-variable annual profit are

\operatorname{TVC}(D,Q)=\frac Q2 IC+\frac DQ S+kD, \qquad \Pi(p,Q)=D(p)p-\operatorname{TVC}(D(p),Q)-f.

Only pairs with $D(p)>0$ and $Q>0$ are feasible. For a fixed demand level, the economic lot size is $Q^*(D)=\sqrt{2DS/(IC)}$ . Substituting it into profit gives Whitin's reduced profit

P(p)=ap^2+bp-\sqrt{2SIC(ap+b)}-k(ap+b)-f.

The paper uses $P$ for annual profit in this section. The Lean development calls the two-variable function profit and the function after optimizing $Q$ reducedProfit.

Formalization targets

The first target is the unique lot-size minimum in Eq. (3), followed by its value in Eq. (4):

\operatorname{TVC}(D,Q^*(D))\leq\operatorname{TVC}(D,Q) \quad(Q>0),\qquad \operatorname{TVC}(D,Q^*(D))=\sqrt{2DSIC}+kD.

Equality in the inequality holds only at $Q=Q^*(D)$ . The next target is the necessary stationarity condition in Eqs. (6)–(7): when $D(p)>0$ and the derivative of $P$ at $p$ is zero,

8a^3p^3+(16a^2b-8ka^3)p^2 +(10ab^2-12ka^2b+2k^2a^3)p +2b^3-4kab^2+2k^2a^2b-SICa^2=0.

The goal joins these steps at a global joint maximum. If a feasible pair $(p,Q)$ maximizes $\Pi$ over all feasible price and lot-size pairs, then $Q=Q^*(D(p))$ and $p$ satisfies the cubic. The goal is an implication about any joint maximizer; it does not assert that one exists for every demand curve. The cubic is a necessary condition only. Its algebraic roots may include prices that fail the original first-order equation or fail to maximize profit.

Significance

The result gives a concrete relation between a price chosen to maximize annual profit and the ordering cost and carrying charge of the inventory system. The lot-size formula alone optimizes cost at a fixed demand rate. The cubic makes the demand response to price and the resulting inventory cost visible in the price condition. It also specifies what can be inferred from the calculation: an optimal price must satisfy the equation, while selecting an optimum from candidate roots remains a separate question.

The paper already supplies the mathematical result. The formalization task is to represent the joint optimization and verify its necessary conditions in Lean, together with the cost identity on which the reduced-profit expression rests. The published Prove2Me definition InventoryControl_eoq already provides the classical EOQ cost and square-root quantity; this mission uses its cost function and adds Whitin's demand curve and profit. Related inventory results for backorders and multilevel systems describe different models and do not replace the targets here.

Difficulty

At a fixed price, choosing the lot size involves both a term proportional to $Q$ and one proportional to $1/Q$ . The optimality statement needs a global inequality and a unique equality case, not merely the observation that a derivative vanishes. After substituting that quantity, the reduced profit contains a square root of the demand curve. Its derivative is meaningful on positive demand, and turning its stationarity equation into the displayed cubic loses information when an equation is squared. A proof therefore has to preserve the implication from optimality to the cubic without promoting all cubic roots to optima.

Formalization scope

The model uses real prices, real demands, and real lot sizes; it does not round order quantities to integers. The hypotheses $S,I,C>0$ make explicit the positive cost and carrying-charge conventions of Section 2. Neither $k$ nor $f$ is assigned a sign, and no sign is imposed on $a$ or $b$ . The conditions $Q>0$ and $D(p)>0$ apply to every cost or profit comparison. They exclude Lean's total value for division by zero and the zero value assigned by Real.sqrt to a negative argument. The goal quantifies over every feasible pair in a joint maximum of the original profit, so optimizing $Q$ is part of its content. Defining profit only by the reduced formula would erase that claim.

The definitions comprise linear demand, total variable cost, two-variable profit, and reduced profit. The classical EOQ cost comes from the existing InventoryControl_eoq definition; the model-specific layer is small and can be reused in further work on pricing with inventory costs. The theorem targets welcome proofs of the global lot-size inequality, the minimized-cost identity, the stationary cubic, and their combination at a joint maximizer. The paper's quantity-discount footnote is outside this scope because it leaves the revised purchase and carrying-cost model unspecified.

Selected references

T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 1955, pp. 61–68. DOI: 10.1287/mnsc.2.1.61.

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

On General Minimax Theorems 2: Kneser–Fan — If f Is Concave-Convexlike and u.s.c. in μ on Compact M, Then sup inf f = inf sup fResearch Paper

Motivation

A minimax theorem asserts that for a real function $f(\mu,\nu)$ of two variables the order of optimization does not matter:

\sup_{\mu}\inf_{\nu} f(\mu,\nu)=\inf_{\nu}\sup_{\mu} f(\mu,\nu).

In game theory it says that a two-person zero-sum game has a value; in optimization it is the engine behind Lagrangian duality, robust optimization (exchanging the decision and the adversary) and distributionally robust and online-learning bounds, where a worst case over a family of distributions is exchanged with a minimization over decisions.

Most minimax theorems require linear structure: $f$ concave in $\mu$ and convex in $\nu$ on convex sets. K. Fan observed that a much weaker, purely order-theoretic condition suffices, which he called concavelike and convexlike, and which makes sense on sets with no linear structure at all. This is the setting needed when the strategy sets are, for instance, sets of stopping times, of measurable policies, or of combinatorial objects whose mixtures are only "dominated" by another member of the set.

Timeline:

1928 — J. von Neumann proves the minimax theorem for bilinear payoffs on simplices (finite matrix games).
1952 — H. Kneser proves it for $f$ concave-convex on a compact convex set and a convex set, with $f$ upper semicontinuous in the compact variable (Kneser, C. R. Acad. Sci. Paris 234, 1952; reference [6] of Sion's paper).
1953 — K. Fan replaces concavity-convexity by concavelikeness-convexlikeness and removes the linear structure (Fan 1953).
1958 — M. Sion, in On general minimax theorems (Sion 1958), proves the quasi-concave-convex minimax theorem and, in §4, re-derives the Kneser–Fan theorem from a finite-reduction criterion (his Theorems 4.1, 4.1′, 4.2, 4.2′).

Setting

Let $M$ and $N$ be arbitrary sets and $f:M\times N\to\mathbb R$ a real-valued function; $\mu\in M$ is the maximizing variable and $\nu\in N$ the minimizing one.

$f$ is concavelike in $M$ if for all $\mu_1,\mu_2\in M$ and $0\le t\le1$ there is one $\mu\in M$ with $t f(\mu_1,\nu)+(1-t)f(\mu_2,\nu)\le f(\mu,\nu)$ for every $\nu\in N$ .
$f$ is convexlike in $N$ if for all $\nu_1,\nu_2\in N$ and $0\le t\le1$ there is one $\nu\in N$ with $t f(\mu,\nu_1)+(1-t)f(\mu,\nu_2)\ge f(\mu,\nu)$ for every $\mu\in M$ .
$f$ is concave-convexlike if it is both.

In each definition the witness depends only on the two given points and on $t$ , never on the point of the other space. The two values compared are the extended reals

\sup\inf f=\sup_{\mu\in M}\inf_{\nu\in N}f(\mu,\nu),\qquad \inf\sup f=\inf_{\nu\in N}\sup_{\mu\in M}f(\mu,\nu),

which may be $\pm\infty$ . In the Lean development these are Concavelike f, Convexlike f, ConcaveConvexlike f, supInf f and infSup f in the namespace SionMinimax.KneserFan. The inequality $\sup\inf f\le\inf\sup f$ always holds; the theorems assert the reverse.

Formalization targets

Goal: the Kneser–Fan theorem (Theorem 4.2, p. 175)

If $M$ is a compact topological space, $f$ is concave-convexlike, and $\mu\mapsto f(\mu,\nu)$ is upper semicontinuous for each $\nu\in N$ , then

\sup\inf f=\inf\sup f.

No structure on $N$ and no linear structure on $M$ are assumed.

Milestones

Theorem 4.1′ (p. 175): if $f$ is concave-convexlike and for every real $c>\sup\inf f$ there is a finite $Y\subset N$ such that every $\mu\in M$ has some $y\in Y$ with $f(\mu,y)<c$ , then $\sup\inf f=\inf\sup f$ .
Theorem 4.1 (p. 175): the dual criterion — for every real $c<\inf\sup f$ a finite $X\subset M$ such that every $\nu\in N$ has some $x\in X$ with $f(x,\nu)>c$ .
Theorem 4.2′ (p. 175): the dual of the goal — $N$ compact and $f(\mu,\cdot)$ lower semicontinuous for each $\mu$ .

The paper itself states that 4.2 is a special case of 4.1′, which in turn follows from the finite-dimensional minimax theorem. Sion's own minimax theorem (Theorem 3.4 and its Corollary) is already formalized on the platform as FamousTheorems.sion_minimax_theorem and is included in the mission as a reference item.

Significance

The Kneser–Fan theorem is the standard minimax theorem for settings without a natural linear structure. Its finite-reduction form (4.1, 4.1′) isolates the only place where topology enters: compactness and semicontinuity are used solely to replace $N$ (or $M$ ) by a finite set, after which the argument is finite-dimensional. Statements of this kind are used to exchange the order of optimization in robust and distributionally robust optimization, in statistical decision theory (existence of least favourable priors, Wald's complete-class theorems) and in learning theory, where the adversary's set is a space of distributions and the learner's set is a space of hypotheses with no convex parametrization.

The theorem is classical and fully proved in the literature. No machine-checked proof of it is known in Mathlib or on the platform: Mathlib contains Sion's quasi-concave-convex theorem (Topology/Sion.lean) and the platform has the bilinear and quasi-convex cases, but neither covers concavelike-convexlike functions, which are independent of quasi-concave-convex ones. This mission produces machine-checked versions of all four §4 statements in the extended reals, including the degenerate cases where values are infinite.

Difficulty

The obvious reduction, "replace $M$ by its convex hull and apply a linear minimax theorem", is unavailable: $M$ and $N$ are bare sets, so there is no convex hull and no mixed strategy to form. Concavelikeness only promises that a mixture of two strategies is dominated by some third strategy, and this has to be iterated to finite mixtures and combined with a separation argument in $\mathbb R^Y$ for a finite $Y$ .

The second difficulty is bookkeeping: the minimax values live in $[-\infty,+\infty]$ , the threshold $c$ is real, and $f$ may be unbounded, so every step comparing a real $c$ with $\sup\inf f$ or $\inf\sup f$ must handle infinite values; a real-valued supremum would silently replace them by $0$ .

Formalization scope

$M$ , $N$ are arbitrary Lean types and $f : M\to N\to\mathbb R$ . For Theorem 4.2 the type $M$ carries an arbitrary topology with CompactSpace M; for 4.2′, $N$ carries one with CompactSpace N. No Hausdorff, metric or linear structure is assumed.
"Upper (lower) semi-continuous in $\mu$ for each $\nu$ " is Mathlib's UpperSemicontinuous (fun μ => f μ ν) (resp. LowerSemicontinuous (fun ν => f μ ν)) on the whole compact space.
$\sup\inf f$ and $\inf\sup f$ are EReal-valued (⨆ μ, ⨅ ν, (f μ ν : EReal) and its dual); the threshold $c$ in 4.1, 4.1′ is a real number compared through the coercion; the finite sets are Finsets chosen after $c$ .
Added reading. Every statement assumes Nonempty M ∨ Nonempty N. When $M=N=\varnothing$ all printed hypotheses hold vacuously (take $X=\varnothing$ or $Y=\varnothing$ ), yet $\sup\inf f=\sup\varnothing=-\infty$ and $\inf\sup f=\inf\varnothing=+\infty$ , so the printed statements fail only in that corner. When exactly one of the sets is empty both sides coincide and that case is kept. No printed slip is corrected; the milestone texts are verbatim.
Ruled out. The concavelike/convexlike witnesses are chosen before the universally quantified point of the other space; reversing the quantifiers would make every function with pointwise maximizers concavelike and the theorems false. The definitions contain no compactness or finite-cover property, and there is no linear structure through which concavity could be substituted for concavelikeness.
Infrastructure. A complete development needs the extension of concavelikeness to finite convex combinations, a finite-dimensional separation (or a finite minimax) lemma for $\mathbb R^Y$ , and lemmas on EReal suprema of real-valued families; these are reusable for any minimax result without linear structure. Contributions proving the milestones independently, or deriving 4.1′ from the referenced Sion theorem by embedding into a simplex, are welcome.

Selected references

M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39, 42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
H. Kneser, Sur un théorème fondamental de la théorie des jeux, Comptes Rendus de l'Académie des Sciences Paris 234, 2418–2420, 1952 (cited as [6] in Sion 1958, https://doi.org/10.2140/pjm.1958.8.171).
H. Nikaidô, On von Neumann's minimax theorem, Pacific Journal of Mathematics 4, 65–72, 1954. https://doi.org/10.2140/pjm.1954.4.65

6 thms3 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research IV: Optimum Phase Times of a Two-Phase Fixed-Time Signal — When the Minimum Cycle Minimizes Average Delay, and the Optimum OtherwiseResearch Paper

Motivation

A fixed-time traffic signal is set by two numbers per phase: how long the green lasts and, through the other phase's green, how long the red lasts. Traffic engineers in the early 1950s set signals by Adams' formula, the shortest cycle that can clear the arriving traffic, on the working assumption that the shortest feasible cycle also gives the least delay. J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259), the paper that also introduced the two Wardrop principles of route choice, tested that assumption analytically for a two-phase signal with uniform arrivals. Appendix IV shows that the shortest cycle is optimal only under an explicit condition on the flows, and gives the optimal cycle when the condition fails. Its numerical example (p. 339) lengthens the cycle by 75 per cent and reduces the overall mean delay by 11 per cent, a case that arises when one phase serves a minor road.

The question was taken up by F. V. Webster's 1958 delay formula and optimum-cycle rule for random arrivals, which became the standard practice; the deterministic two-phase analysis here is its uniform-flow precursor.

Setting

A two-phase signal serves two streams. For phase $k \in \{1,2\}$ :

$q_k$ is the arriving flow (vehicles per unit time);
$p_k$ is the saturation flow, the rate at which a queue discharges at minimum headway;
$a_k$ is the lost time, the delay of the first vehicle at the start of green;
$g_k$ is the green time and $r_k$ the red time, with $r_1 = g_2$ and $r_2 = g_1$ .

The totals are $Q = q_1 + q_2$ , $A = a_1 + a_2$ , and the cycle time $c = g_1 + g_2$ . Vehicles do not accumulate indefinitely on phase $k$ when the green, less its lost time, can clear one cycle's arrivals: $q_k c \le p_k(g_k - a_k)$ . Equality on both phases (both greens saturated) gives Adams' formula

c = \frac{A}{1 - q_1/p_1 - q_2/p_2}. \tag{12}

The flow-weighted average delay at the intersection is

T = \frac{1}{2Qc}\left\{\frac{q_1(r_1+a_1)^2}{1 - q_1/p_1} + \frac{q_2(r_2+a_2)^2}{1 - q_2/p_2}\right\}. \tag{16}

Appendix IV changes variables to the effective-red fractions $x = (r_1+a_1)/c$ and $y = (r_2+a_2)/c$ . With

\xi = 1 - \frac{q_1}{p_1},\quad \eta = 1 - \frac{q_2}{p_2},\quad \lambda = \frac{Aq_1}{2Q\xi},\quad \mu = \frac{Aq_2}{2Q\eta},

one has $c = A/(x+y-1)$ , the no-accumulation conditions become $x \le \xi$ and $y \le \eta$ , and

T(x,y) = \frac{\lambda x^2 + \mu y^2}{x + y - 1}.

The feasible region is $F = \{(x,y) : x \le \xi,\ y \le \eta,\ x + y > 1\}$ . Its corner $(\xi,\eta)$ is the minimum cycle (12). The phases are labelled so that $\lambda \ge \mu$ .

Formalization targets

Goal: the optimum phase times

Put

D = \frac{\mu}{\lambda}\eta^2 + 2\xi(1-\eta) - \xi^2, \qquad x_0 = 1 - \eta + \sqrt{(1-\eta)^2 + \frac{\mu}{\lambda}\eta^2}.

For $\lambda \ge \mu > 0$ , $0 < \xi, \eta < 1$ and $\xi + \eta > 1$ :

D > 0 \implies T(\xi,\eta) = \min_{F} T, \qquad D \le 0 \implies (x_0,\eta) \in F \text{ and } T(x_0,\eta) = \min_F T.

At $D = 0$ , $x_0 = \xi$ , so the second formula gives the minimum cycle. This boundary case belongs to the page's final “if this condition is not satisfied” clause.

Milestones (Appendix IV, in the order of the argument)

The partial derivatives at the corner:

\left[\frac{\partial T}{\partial x}\right]_{\xi,\eta} = \frac{\lambda\xi^2 - \mu\eta^2 - 2\lambda\xi(1-\eta)}{(\xi+\eta-1)^2},\qquad \left[\frac{\partial T}{\partial y}\right]_{\xi,\eta} = \frac{\mu\eta^2 - \lambda\xi^2 - 2\mu\eta(1-\xi)}{(\xi+\eta-1)^2}.

If both are negative, $(\xi,\eta)$ minimizes $T$ over $F$ .
When $\lambda \ge \mu$ , $(\xi+\eta-1)^2[\partial T/\partial y]_{\xi,\eta} = -\mu\{2\eta(1-\eta) + (\xi-\eta)^2\} - (\lambda-\mu)\xi^2 < 0$ .
$[\partial T/\partial x]_{\xi,\eta} < 0$ if and only if $D > 0$ .
If $D < 0$ , $x_0$ is the unique root of $\lambda x^2 - \mu\eta^2 - 2\lambda x(1-\eta) = 0$ in $0 < x < \xi$ .

Companions

Adams' formula (12) and the minimality of its cycle; the change of variables from (16) to $T(x,y)$ ; and the translation into the original quantities: $\lambda \ge \mu$ iff $1/q_1 - 1/p_1 \le 1/q_2 - 1/p_2$ , $D > 0$ iff $q_1(1 - q_1/p_1) - q_2(1 - q_2/p_2) < 2q_1q_2/p_2$ , and the delay-minimizing cycle $c = A/\sqrt{(q_2/p_2)^2 + (q_2/q_1)(1 - q_1/p_1)(1 - q_2/p_2)}$ when $D \le 0$ .

Significance

The result gives a closed-form test for whether the minimum cycle is the delay-optimal cycle of a two-phase fixed-time signal with uniform flows, and the optimal cycle when it is not. It shows that the common assumption, shortest cycle equals best cycle, can fail, and identifies when: the test depends on the flow ratios and on which phase is the heavier one in the sense of $1/q - 1/p$ . In the failing case the optimum keeps the minor phase saturated and lengthens only the major phase's green.

The result is proved on the page by a short calculus argument. It has not been machine-checked anywhere known to this mission. The formal work is to establish the global optimality claims behind the page's local reasoning, to pin down the hypotheses the page uses silently (positivity of flows and lost times, the capacity condition, the phase labelling), and to correct the printed slips listed under Formalization scope. The reparametrization and the original-quantity forms tie the abstract statement back to signal settings.

Difficulty

The page argues locally: at the corner both partial derivatives are negative, and "the only possible changes in $x$ and $y$ are reductions", so $T$ is a minimum. Negative partial derivatives at a corner of the region show that no small reduction helps; they do not by themselves exclude a better point far from the corner. The global claim needs a property of $T$ on the whole region $x + y > 1$ , not just at one point. The second case has the same issue: the page locates a critical point on the edge $y = \eta$ and needs, in addition, that no interior or other boundary point does better. The algebra of the corner criterion is routine; the global minimality is the step that carries the content.

Formalization scope

All quantities are real numbers. The objects are delayT lam mu x y $= T(x,y)$ , feasibleXY xi eta $= F$ , cornerD $= D$ , edgeRoot $= x_0$ , the maps xiOf, etaOf, lamOf, muOf from the flows to $\xi,\eta,\lambda,\mu$ , and avgDelay16, the right side of (16). Derivatives are stated with HasDerivAt on the one-variable sections of $T$ ; minimality is the explicit inequality $T(\cdot) \le T(z)$ for every $z \in F$ .

Conventions and added hypotheses, each presupposed by the page:

$x + y > 1$ is part of $F$ : it is $c > 0$ through $c = A/(x+y-1)$ . Without it, $T$ would take Lean's junk value $0$ on the line $x + y = 1$ and negative values beyond it, and the minimum would be meaningless.
$\xi + \eta > 1$ , i.e. $q_1/p_1 + q_2/p_2 < 1$ : the minimum cycle is positive and $F$ is nonempty. Without it both parts of the goal hold vacuously.
$0 < \xi$ , $0 < \eta$ ( $q_k < p_k$ ), $\lambda, \mu > 0$ , and the labelling $\lambda \ge \mu$ , which the page imposes by interchanging the phases. Case 1 of the goal is false without $\lambda \ge \mu$ .
In the companions: $0 < q_k < p_k$ , $Q = q_1 + q_2 > 0$ , and positive total lost time $A$ (or $A \ne 0$ for Adams' formula), which keeps the divisions in (12) and in $c = A/(x+y-1)$ from being junk.

The goal is stated in $\lambda,\mu,\xi,\eta$ alone, which is all Appendix IV uses; the companions connect them to the flows.

Printed slips, corrected in the Lean and named in each item: $(\xi+\eta)^2$ for $(\xi-\eta)^2$ in the expression for $\partial T/\partial y$ (p. 359); the range " $0 < x < \eta$ " for $0 < x < \xi$ (p. 359); " $\ge$ " for $\le$ in the original-quantity form of $\lambda \ge \mu$ (p. 359); and " $c + a$ ", " $a/(x+y-1)$ ", " $\eta = 1 - q_1/p_1$ " for $c + A$ , $A/(x+y-1)$ , $\eta = 1 - q_2/p_2$ (p. 358).

Stating the goal as "the partial derivatives at $(\xi,\eta)$ are negative" would replace the theorem by its mechanism; the goal is minimality over the whole feasible region. Not covered: the delay formula (13) and its heuristic derivation in Appendix III, the approximation (14), and the rounded numerical example of p. 339.

Contributions are welcome on every milestone and companion. General facts about functions of the form $(\lambda x^2 + \mu y^2)/(x+y-1)$ on the half-plane $x + y > 1$ are reusable beyond traffic signals.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II, 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
A. J. H. Clayton, Road traffic calculations, Journal of the Institution of Civil Engineers 16 (1941), p. 247. Cited by Wardrop (his ref. 7) as the source of Adams' formula and of the delay formulae.
F. V. Webster, Traffic signal settings, Road Research Technical Paper No. 39, HMSO, London, 1958.

7 thms3 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Revenue Management Under a General Discrete Choice Model of Consumer Behavior 3: The Multinomial Logit Model Has the Nesting-by-Fare-Order PropertyResearch Paper

Motivation

Airline and hotel revenue management sells one perishable resource (seats on a flight, rooms on a night) through several fare products at different prices. The classical models of Littlewood (1972), Belobaba (1989) and Lee and Hersh (1993) assume independent demand: a customer who wants fare class $j$ either buys class $j$ or leaves, whatever else is on offer. Under that assumption the optimal booking policy is nested by fare order: at any time the firm opens a top segment $\{1, \dots, k\}$ of the fare ladder, and closes classes from the cheapest upwards as capacity becomes scarce.

Real customers substitute. If the cheap fare is closed, some buy up; if a mid-priced fare is open, some buy down. Talluri and van Ryzin (working paper 2001; published as Management Science 50(1), 2004) model this with a general discrete choice model: the firm chooses which set $S$ of fares to offer, and a customer buys product $j$ with probability $P_j(S)$ . Their §3 asks when the fare-order nesting of the independent model survives under choice behaviour. They give a characterization (Theorem 2, the subject of mission 2 of this series) and verify it for two models: the independent demand model (Proposition 5) and the multinomial logit (MNL) model (Proposition 6). The MNL model is the standard choice model in travel demand forecasting and marketing (Ben-Akiva and Lerman, 1985), so Proposition 6 says that the fare-order structure airlines already implement remains optimal under the most widely used substitution model.

Setting

There are $n$ fare products $N = \{1, \dots, n\}$ with revenues $r_1 \ge r_2 \ge \dots \ge r_n \ge 0$ . A choice model assigns to each offer set $S \subseteq N$ numbers $P_j(S) \ge 0$ with $\sum_{j\in S} P_j(S) \le 1$ and $P_j(S) = 0$ for $j \notin S$ ; the remainder $P_0(S) = 1 - \sum_{j\in S} P_j(S)$ is the no-purchase probability. Write $Q(S) = \sum_{j\in S} P_j(S)$ for the purchase probability and $R(S) = \sum_{j \in S} r_j P_j(S)$ for the expected revenue.

The complete sets are $A_k = \{1, \dots, k\}$ , $k = 0, 1, \dots, n$ , with $A_0 = \emptyset$ . A choice model has the nesting-by-fare-order property (Definition 4) if

$Q$ is increasing: $Q(S) \le Q(T)$ whenever $S \subseteq T$ ; and
for every $x_1 \ge x_2 \ge \dots \ge x_n$ , the problem $\max_{S\subseteq N} \sum_j x_j P_j(S)$ has an optimal solution that is complete.

In the single-resource dynamic program, $x_j = r_j - \Delta V$ for the marginal value $\Delta V$ of capacity, so condition 2 says that the optimal offer set is always a top segment of the fare ladder.

The MNL model with preference weights $w_j = e^{u_j} > 0$ and no-purchase weight $w_0 = 1$ is

P_j(S) = \frac{w_j}{\sum_{i\in S} w_i + 1}, \qquad j \in S. \qquad (14)

The independent model is $P_j(S) = q_j$ for $j \in S$ . A set $T$ is dominated (Definition 1) if some randomization over offer sets has no larger expected purchase probability and strictly larger expected revenue, or strictly smaller purchase probability and no smaller revenue.

Formalization targets

Goal: Proposition 6, in the form its proof establishes

\forall\, w \in \mathbb{R}_{>0}^n:\quad P = \mathrm{MNL}(w) \text{ has the nesting-by-fare-order property.}

This leaves the fares unrestricted: condition 2 quantifies over all ordered value vectors $x$ , so the goal holds for every fare ladder at once.

Milestones

Lemma 5: if $\theta f(y_1) + (1-\theta) f(y_3) = f(y_2)$ for $f(y) = y/(y+1)$ , the same holds for $g(y) = 1/(y+1)$ .
The MNL purchase probability $Q(S) = W(S)/(W(S)+1)$ , $W(S) = \sum_{i\in S} w_i$ , is increasing.
For an incomplete $T$ : an index $k^*$ with $W(A_{k^*}) \le W(T) < W(A_{k^*+1})$ , and a weight $\theta \in [0,1]$ solving (15).
With the weights $\theta$ on $A_{k^*}$ and $1-\theta$ on $A_{k^*+1}$ : $\bar P_j(\alpha) \ge P_j(T)$ for $j \le k^*$ , and the prefix sums beyond $k^*$ equal $Q(T)$ .
Theorem 2, sufficiency direction: increasing $Q$ plus such majorizing mixtures for every incomplete $T$ give the nesting-by-fare-order property.

Companions

Proposition 6, first sentence, under strictly decreasing fares: every nondominated set is complete.
Proposition 5: the independent model has the nesting-by-fare-order property.

Significance

The result. Proposition 6 turns a structural question about an exponentially large dynamic program (the firm chooses among $2^n$ offer sets in every period) into the familiar one-dimensional policy of opening fares from the top. For MNL demand, the optimal control is described by $n$ protection levels, which is how airline reservation systems already operate; the paper's later remark (17) gives the opening condition for fare $k+1$ . Without it, a firm whose customers substitute according to MNL would have no guarantee that fare-ordered nesting is not leaving revenue on the table.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked proof of Proposition 6, a checked sufficiency direction of Theorem 2 that applies to any choice model, and the independent-demand case (Proposition 5). The literal wording of Proposition 6 ("the only nondominated sets are the complete sets") is false when fares tie; the mission records the corrected statement under strictly decreasing fares.

Difficulty

The obvious approach compares an incomplete set $T$ directly with a single complete set, and it fails: under MNL, adding a fare changes every other fare's probability through the common denominator, so no single complete set need match $T$ 's purchase probability while selling at least as much of every high fare. A comparison through randomizations over complete sets is needed, and a weight that matches $T$ 's total purchase probability does not, for a general choice model, match the individual product probabilities as well. The final comparison must also hold for every ordered value vector $x$ , including vectors with negative entries, for which the empty set can be the only optimum.

Formalization scope

Products are Fin n (index $j-1$ for fare $j$ ); a choice model is P : Finset (Fin n) → Fin n → ℝ with the published RevenueManagement.IsChoiceModel (nonnegativity, total at most one) plus SupportedOn P ( $P_j(S) = 0$ off $S$ , the model's convention on p. 5). $A_k$ is complete n k = {j | j.val < k} for $k \in \{0, \dots, n\}$ ; the empty set $A_0$ counts as complete, and the mixture weights $\alpha$ are indexed by $\{0, \dots, n\}$ . The page indexes complete sets as $k = 1, \dots, n$ ; without $A_0$ , condition 2 fails for every model when all $x_j < 0$ , where only $\emptyset$ is optimal. The order $x_1 \ge \dots \ge x_n$ is Antitone x. The paper's weight $\lambda$ is written $\theta$ , since λ is reserved in Lean.

Standing hypotheses and pins: MNL weights $w_j > 0$ ( $w_j = e^{u_j}$ ); for the independent model $q_j \ge 0$ and $\sum_j q_j \le 1$ , so that it is a probability function; strictly decreasing fares StrictAnti r for the nondominated-set companion only, because with $r_1 = r_2 > 0$ and $w_1 = w_2$ the incomplete set $\{2\}$ is nondominated.

The goal is the full Definition 4 with both conditions; it may not be weakened to condition 1 alone, to condition 2 for nonnegative $x$ , or to a statement that assumes condition (ii) of Theorem 2 or the existence of $k^*$ . The "Moreover" sentence of Propositions 5 and 6 (nested allocation policies, Definition 3) is not formalized. Theorem 2's sufficiency half is restated here because draft items cannot import the drafts of mission 2; the definitions of complete sets and the property are shared verbatim with that mission.

Contributions welcome: proofs of the milestones, a general summation-by-parts lemma for majorized vectors (reusable beyond this mission), and the converse of Theorem 2 via Farkas' lemma.

Selected references

K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, working paper, October 21, 2001 (UPF Economics Working Paper 533); published in Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
M. Ben-Akiva, S. Lerman, Discrete Choice Analysis: Theory and Application to Travel Demand, MIT Press, 1985. https://mitpress.mit.edu/9780262536400/
T. C. Lee, M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3):252–265, 1993. https://doi.org/10.1287/trsc.27.3.252
A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-0-387-68276-1

11 thms3 active usersReviewed

Completed

Algorithmic Game Theory Topology·Captain: mikedeng1

On General Minimax Theorems 1: For a Minimal Finite Y with Every f(·, y) Quasi-Concave and u.s.c. on Convex M, One μ₀ ∈ M Has f(μ₀, y) < c for All y ∈ YResearch Paper

Motivation

A minimax theorem asserts that, for a function $f(\mu, \nu)$ of two variables,

\sup_{\mu \in M} \inf_{\nu \in N} f(\mu, \nu) = \inf_{\nu \in N} \sup_{\mu \in M} f(\mu, \nu).

Such equalities are the basis of zero-sum game theory, of Lagrangian duality in optimization, of robust optimization, and of minimax lower bounds in statistics and online learning. Maurice Sion's 1958 paper On general minimax theorems proved the version most often cited today: $M$ and $N$ convex subsets of topological vector spaces, one of them compact, $f$ quasi-concave and upper semicontinuous in $\mu$ , quasi-convex and lower semicontinuous in $\nu$ .

Sion's theorem itself is already machine-checked: Mathlib's Sion.minimax proves it, following the elementary argument of Komiya (1988), and the platform holds it as FamousTheorems.sion_minimax_theorem. Sion's own proof is different. It runs through an open-cover form of the Knaster–Kuratowski–Mazurkiewicz (KKM) theorem, a Helly-type fact about $n+1$ points in low dimension, and a lemma about minimal finite covers (Lemma 3.3). That route has not been formalized. This mission formalizes its ingredients, with Lemma 3.3 as the goal.

Timeline:

1928: von Neumann proves the minimax theorem for bilinear payoffs on simplices (mixed strategies of matrix games).
1929: Knaster, Kuratowski and Mazurkiewicz prove the KKM covering theorem for closed sets.
1952–1953: Kneser and Fan extend the minimax theorem to concave-convex and concavelike-convexlike functions on compact sets.
1958: Sion proves the quasi-concave-convex version with semicontinuity, by the KKM route.
1988: Komiya gives an elementary proof avoiding KKM; it is the proof formalized in Mathlib.

Setting

Let $E$ be a real topological vector space: a real vector space with a topology for which addition and scalar multiplication are continuous. A set $M \subseteq E$ is convex if it contains the segment between any two of its points. The convex hull $\ulcorner X \urcorner$ of a set $X$ is the smallest convex set containing it.

A real function $g$ on a convex set $M$ is quasi-concave on $M$ if every superlevel set $\{\mu \in M : g(\mu) \ge r\}$ is convex, and quasi-convex if every sublevel set $\{\mu \in M : g(\mu) \le r\}$ is convex. It is upper semicontinuous (u.s.c.) on $M$ if every strict sublevel set $\{\mu \in M : g(\mu) < r\}$ is open in the topology $M$ inherits from $E$ ; lower semicontinuous (l.s.c.) is the mirror notion.

Let $Y$ be a finite set, $c$ a real number, and $f$ a real function on $M \times Y$ . Say that $Y$ has property P if for each $\mu \in M$ there is a $y \in Y$ with $f(\mu, y) < c$ , and that $Y$ is minimal for P if no proper subset of $Y$ has P.

An $n$ -dimensional simplex with vertices $a_0, \dots, a_n$ is the convex hull of $n+1$ affinely independent points.

Formalization targets

Goal: Lemma 3.3 (p. 173)

Let $M \subseteq E$ be nonempty and convex, $Y$ finite, and $f(\cdot, y)$ quasi-concave and u.s.c. on $M$ for each $y \in Y$ . If $Y$ is minimal for P, then

\exists\, \mu_0 \in M \;\; \forall y \in Y: \quad f(\mu_0, y) < c.

The lemma makes no compactness or finite-dimensionality assumption on $M$ ; that generality is what lets Sion apply it on the convex hull of a finite set inside an arbitrary topological vector space.

Milestones

Theorem 3.2 (p. 173). If $\mathfrak A = \{a_0, \dots, a_n\}$ are $n+1$ points in a real vector space of dimension $k < n$ , then $\bigcap_{i=0}^n \ulcorner \mathfrak A - \{a_i\} \urcorner \ne \emptyset$ .
Theorem 3.1 (p. 173). If $S$ is an $n$ -simplex with vertices $a_0, \dots, a_n$ and $A_0, \dots, A_n$ are open in the ambient space, $S \subseteq \bigcup_i A_i$ , each $S - A_i$ is convex, and $a_i \notin A_j$ for $i \ne j$ , then $\bigcap_{i} A_i \neq \emptyset$ .
Lemma 3.3′ (p. 173). The dual of the goal: quasi-convex, l.s.c. in the second variable, with $>$ in place of $<$ .
Remark 3.6 (p. 174). The explicit function on $[0,1]^2$ , quasi-concave-convex and l.s.c. in $\nu$ but not u.s.c. in $\mu$ , with $\sup\inf f = 0 < 1 = \inf\sup f$ .

Sion's Theorem 3.4 and the Corollary on p. 174 (the minimax theorem) enter the mission as the existing, proved platform item FamousTheorems.sion_minimax_theorem.

Significance

Lemma 3.3 is a finite, one-sided statement that already contains the full strength of the quasi-concave case: a finite family of "threats" $y \in Y$ , none of which can be dropped, can be beaten simultaneously by one point $\mu_0$ . On p. 174 Sion derives the minimax theorem from Lemma 3.3 and Lemma 3.3′ by reducing open covers to minimal finite ones, alternately on each side. Theorem 3.1 is an open-set KKM theorem with a convexity condition on complements, a covering principle of independent use in fixed-point theory and equilibrium existence. Remark 3.6 shows that the semicontinuity hypotheses are not decorative.

On the formal side, the minimax theorem is proved in Mathlib by another route, so nothing in this mission is needed to know that Sion's theorem is true. What the mission adds is the infrastructure of the original proof: a KKM-type theorem (absent from Mathlib and from the platform), a Helly-type statement about $n+1$ points, and the minimal-cover lemma. None of these has a machine-checked proof today. A formalized open KKM theorem is reusable for Fan's lemma, for Gale–Nikaido–Debreu type existence results and for other covering arguments.

Difficulty

The obvious approach to Lemma 3.3 is induction on $|Y|$ , using quasi-concavity to combine points that are good for subfamilies. It fails because quasi-concavity gives control over superlevel sets $\{f \ge c\}$ only, so the union of two "bad" sets is not controlled, and nothing forces two partial witnesses to have a common improvement on the segment between them. The lemma is genuinely topological: without upper semicontinuity it is false (Remark 3.6 exhibits the resulting failure of the minimax equality).

The topological content sits in Theorem 3.1. Neither Mathlib nor the platform has a KKM theorem (the platform has Brouwer's fixed-point theorem), and the passage from the classical closed-set KKM theorem to the open-set form, and from a simplex inside a possibly non-Hausdorff topological vector space to the standard simplex, both need care: the topology induced on a finite-dimensional subspace need not be the Euclidean one.

Formalization scope

The ambient space is a real topological vector space: [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], the class of Mathlib's Sion file. No Hausdorff or finite-dimensionality assumption is made. The paper never names the ambient space; "convex set" is read as a convex subset of such a space.
Quasi-concavity, quasi-convexity and semicontinuity are Mathlib's QuasiconcaveOn, QuasiconvexOn, UpperSemicontinuousOn, LowerSemicontinuousOn, all relative to the set $M$ or $N$ .
$f$ is typed $E \to \iota \to \mathbb R$ (or $\iota \to E \to \mathbb R$ ) and $Y$ is a Finset ι; values off $M \times Y$ are irrelevant. Minimality is "no strict sub-Finset has property P".
Added hypothesis $M \ne \emptyset$ in Lemma 3.3 and $N \neq \emptyset$ in Lemma 3.3′: with $M = Y = \emptyset$ the hypotheses hold vacuously and the conclusion fails.
Theorem 3.1 uses the page's ambient openness hypothesis and nonempty intersection conclusion. In the application to Lemma 3.3, relatively open strict sublevel sets on $M$ must be represented by ambient open sets before restricting to the simplex.
Theorem 3.2 takes the points as an injective family (encoding " $n+1$ points") and $\mathfrak A - \{a_i\}$ as a set difference; dimension is linear dimension (Module.finrank).
Remark 3.6 formalizes only the checkable claims about the example, with $\sup\inf$ and $\inf\sup$ over the subtype $[0,1]$ in EReal; "cannot be removed nor appreciably weakened" is informal and omitted.
Trivializing formalizations are ruled out: minimality is not defined in terms of the conclusion, and $M$ is neither finite-dimensional nor compact.

Contributions welcome: a formal KKM theorem (closed and open versions), Theorem 3.2 from Mathlib's Convex.helly_theorem, and proofs of the milestones in any order.

Selected references

M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
B. Knaster, C. Kuratowski, S. Mazurkiewicz, Ein Beweis des Fixpunktsatzes für n-dimensionale Simplexe, Fundamenta Mathematicae 14, 132–137, 1929. https://doi.org/10.4064/fm-14-1-132-137
K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1), 42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
H. Kneser, Sur un théorème fondamental de la théorie des jeux, Comptes Rendus de l'Académie des Sciences 234, 2418–2420, 1952.
H. Komiya, Elementary proof for Sion's minimax theorem, Kodai Mathematical Journal 11(1), 5–7, 1988. https://doi.org/10.2996/kmj/1138038812
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 295–320, 1928. https://doi.org/10.1007/BF01448847

6 thms3 active usersReviewed

Completed

Complexity Theory Linear Optimization Operations Research·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 1: The Predictor–Corrector Algorithm Between N₂(1/4) and N₂(1/2) Attains Precision t in O(√n·t) IterationsResearch Paper

Motivation

Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.

The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.

Setting

Fix an integer $n\ge1$ of variables, an arbitrary number $m$ of equality constraints, a real matrix $A\in\mathbb R^{m\times n}$ , and vectors $b\in\mathbb R^m$ and $c\in\mathbb R^n$ . The primal problem minimizes $c^Tx$ over $Ax=b$ , $x\ge0$ . Its dual problem maximizes $b^Ty$ over $A^Ty+s=c$ , $s\ge0$ . The dual slack is $s$ . The development reuses a published general-form LP model and specializes it to this pair.

The strictly feasible pairs $F^0$ are the pairs $(x,s)$ satisfying the two feasibility systems for some dual multiplier $y$ , with every coordinate of $x$ and $s$ strictly positive. The multiplier is allowed to vary with the pair. Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ , and $e$ for the vector of ones. The duality measure is $\mu=x^Ts/n$ . For $0<\beta<1$ , the Euclidean central-path neighborhood is

N_2(\beta)=\{(x,s)\in F^0:\|Xs-\mu e\|_2\le\beta\mu\}.

The search direction $(d_x,d_y,d_s)$ at $(x,s)$ with parameter $\gamma$ solves the three equations $Sd_x+Xd_s=\gamma\mu e-Xs$ , $Ad_x=0$ , and $A^Td_y+d_s=0$ . A step of length $\theta$ yields $(x+\theta d_x,s+\theta d_s)$ . Algorithm 1 begins in $N_2(1/4)$ . It takes a predictor direction with $\gamma=0$ to the greatest step whose entire path remains in $N_2(1/2)$ , then takes one full corrector direction with $\gamma=1$ . The resulting pair starts the next iteration. The algorithm stops when $x^Ts\le2^{-t}$ ; its starting gap is at most $2^t$ report, pp. 4 and 6–7.

Formalization targets

Theorem 1: termination

For every real precision parameter $t$ , every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration $k$ with

k\le\left\lceil2(\log2)8^{1/4}\sqrt n\,t\right\rceil, \qquad (x^k)^Ts^k\le2^{-t}.

The paper states the iteration order as $O(\sqrt n\,t)$ . The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.

Source milestones

The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.

Significance

Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with $\sqrt n$ , rather than with $n$ , in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.

The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.

Difficulty

The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products $x_js_j$ away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.

Formalization scope

Vectors are functions on Fin n, and $A$ is a finite matrix. The report's indices $1,\ldots,n$ correspond to Lean indices $0,\ldots,n-1$ . The norm in $N_2$ and in Lemmas 1–2 is explicitly $\ell_2$ : Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and $\log$ is natural logarithm. The hypothesis $n\ge1$ gives meaning to $\mu=x^Ts/n$ ; no sign condition on $t$ is imposed, since for $t\le0$ the starting pair already meets the stopping test.

The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at $n=1$ there may be no continuing run under this literal algorithm rule; the goal retains $n\ge1$ and makes this limitation explicit. The denominator $\|Pq\|_2$ in Lemma 4 can vanish. The formal lower bound uses its limiting value $1/2$ in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes $n\ge2$ , because its printed lower bound on the predictor length fails at $n=1$ .

The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds $2^{-t}$ ; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. Technical-report PDF. The PDF used here is the technical report, so all page and result indices refer to that version.

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

A Functional Equation and Its Application to Resource Allocation and Sequencing Problems 2: Under Precedence Constraints, All Deadlines Can Be Met iff They Are Met in Order of Modified DeadlinesResearch Paper

Motivation

A single machine must process $n$ jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.

E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.

Setting

There are $n$ jobs $1,\dots,n$ . Job $j$ has a processing time $a_j \ge 0$ and a deadline $d_j \in \mathbb R$ . A sequence $\sigma$ lists every job exactly once; the machine starts at time $0$ and processes the jobs in the order of $\sigma$ , one after another, without idle time. The completion time $C_j(\sigma)$ of job $j$ is the sum of the processing times of $j$ and of all jobs before it in $\sigma$ . Job $j$ is on time in $\sigma$ if $C_j(\sigma) \le d_j$ .

Precedence constraints are a partial order $\rho$ on the jobs (reflexive, antisymmetric, transitive). If $i\rho j$ and $i \ne j$ , job $i$ must precede job $j$ ; such a $j$ is a successor of $i$ , and every job counts as one of its own successors. A sequence is consistent with $\rho$ if no job appears before a job that must precede it. The jobs are numbered so that $i\rho j$ implies $i \le j$ .

For a number $\varepsilon$ the modified deadline of job $j$ is

\bar d_j = \min\{\, d_k \mid j\rho k \,\} + j\varepsilon ,

the earliest deadline among $j$ and its successors, plus a tie-breaking term. The paper takes $\varepsilon$ to be "a small number"; here that means $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$ .

Formalization targets

Goal: the §2 Theorem (p. 78)

Let $\sigma^*$ be the sequence in which $\bar d_j$ increases. Then

\Big(\exists\,\sigma \text{ consistent with } \rho:\ C_j(\sigma) \le d_j\ \ \forall j\Big)\iff C_j(\sigma^*) \le d_j\ \ \forall j .

Milestones (from §2 and the proof of the Theorem, p. 78)

For distinct jobs, $i\rho j \Rightarrow \bar d_i < \bar d_j$ .
The sequence $\sigma^*$ is consistent with $\rho$ (the "if" part of the Theorem).
If $\bar d_j < \bar d_i$ , then $j$ or some successor $k$ of $j$ has $d_k \le d_i$ .
In an on-time sequence consistent with $\rho$ , two adjacent jobs $i, j$ (in this order) with $\bar d_i > \bar d_j$ can be interchanged, and the result is again on time and consistent with $\rho$ .

Significance

The Theorem reduces a question over all $n!$ sequences consistent with $\rho$ to the evaluation of one sequence, and the sequence depends only on the deadlines and on $\rho$ , not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ( $\rho$ the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for $1\mid prec\mid f_{\max}$ .

The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.

Difficulty

The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job $i$ completes when job $j$ used to complete, but $d_i$ need not be at least $d_j$ : one must find a successor of $j$ that is later in the sequence, on time, and due no later than $i$ . That step uses the smallness of $\varepsilon$ : with a large $\varepsilon$ the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, $a = (2,4,3)$ , $d = (7,9,8)$ , $\varepsilon = 3$ ). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into $\sigma^*$ , a bubble-sort argument over lists.

Formalization scope

Jobs are Fin n, 0-based: the Lean job j is the paper's job $j+1$ , and the tie-break is $((j:\mathbb N)+1)\varepsilon$ . Processing times and deadlines are real.
Sequences and completion times are the published platform definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time $0$ , no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with $\rho$ is the published LawlerPrec.MinMax.IsFeasible.
The modified deadline minimizes over insert j {k | ρ j k}, which is nonempty; for the reflexive $\rho$ of the paper this is $\{k \mid j\rho k\}$ ("considering a job to be one of its own successors").
Explicit readings of the paper's phrases:
- " $\varepsilon$ is a small number": $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$ . A fixed $\varepsilon$ is quantified universally, not hidden under an existential.
- "the sequence obtained by ordering jobs according to increasing values of $\bar d_j$ ": any duplicate-free list of all jobs along which $\bar d_j$ strictly increases. Under the hypotheses the $\bar d_j$ are distinct, so exactly one such list exists.
- "iρj implies $\bar d_i < \bar d_j$ ": stated for $i \ne j$ , since $\rho$ is reflexive.
- The pair condition "a consecutive pair with $\bar d_i > \bar d_j$ " of milestone 3 is dropped, since the claim does not use it.
Added hypothesis: $a_j \ge 0$ . The paper uses it tacitly (" $j$ will remain on time since it will be earlier in the sequence") and the Theorem is false without it.
The milestones assume only what they use (for instance, milestone 1 needs transitivity, the numbering and $\varepsilon > 0$ ). The goal assumes the full partial order of the paper.
Trivializing formalizations ruled out: $\varepsilon = 0$ or an unconstrained $\varepsilon$ ; a minimum over a possibly empty set, which Lean would assign a junk value; completion times not tied to the order of the list; and dropping "consistent with the precedence constraints" from the left-hand side, which turns the Theorem into a false variant of Jackson's rule.
Not in scope: the "order of computational steps" remarks, §3 and the later sections (other missions of this series).

Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's $1\mid prec\mid f_{\max}$ theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.

Selected references

E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5) (1973) 544–546. https://doi.org/10.1287/mnsc.19.5.544

8 thms3 active usersReviewed

Missions

Semidefinite Programming 2: If Every Step Lowers the Potential φ by δ > 0, Then After k ≥ (ν√n log(1/ε) + ψ(x⁽⁰⁾, Z⁽⁰⁾))/δ Steps the Duality Gap Is at Most ε Times Its Initial ValueResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Monotone Comparative Statics II: f Is Quasisupermodular If and Only If a Strictly Increasing Transformation Makes It Supermodular on Every Sublattice {x₁, x₂, x₁ ∨ x₂, x₁ ∧ x₂}Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 165)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Learning Models with Uniform Performance via Distributionally Robust Optimization 2: A Minimax Lower Bound of Order n^(−1/2) ∨ n^(−1/k*) for Estimating the Cressie–Read Robust Risk (Theorem 3)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bounded Rationality in Newsvendor Models V: If σ_T ≤ Σσ_i and σ_T ≥ σ_i, Pooling Strictly Lowers the Expected Cost of Logit Newsvendors with Normal DemandsResearch Paper

Motivation

Setting

Formalization targets

Strict pooling reduction

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

Primal-dual subgradient methods for convex problems 1: Dual Averaging Keeps the Gap Below β_{k+1}D + (1/2σ)Σλᵢ²‖gᵢ‖²_*/βᵢ and Its Iterates BoundedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 9)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 2: The Adaptive-Step Algorithm in N∞(β) or N∞⁻(β) with γ ≤ 2(1 − β) Attains Precision t in O(nt) IterationsResearch Paper

Why wide neighbourhoods

Setting

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Régularisation d'inéquations variationnelles par approximations successives II: The Proximal Regularization of a Convex Minimization Problem Is a Minimizing SequenceResearch Paper

Motivation

Setting

Formalization targets

Existence for (12) and well-posedness of (13)

Goal: Théorème 3

Stronger: Remarque 1

Significance

Difficulty

Formalization scope

Selected references

Strongly Regular Generalized Equations IV: Strong Second-Order Sufficiency and Linearly Independent Binding Gradients Make the KKT Generalized Equation Strongly RegularResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (p. 56)

Milestones

Significance

Difficulty

Formalization scope

Goal: $\psi'$ solves the bottleneck traveling salesman problem