Optimization · Prove2Me

Linear Optimization Operations Research·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 3: If (LP) and (LD) Have Interior Feasible Points, Every Self-Complementary Solution of (HLP) Has τ* > 0Research Paper

Motivation

Linear programming algorithms often compute a solution to an auxiliary problem before extracting a solution to the original primal and dual pair. For a homogeneous self-dual formulation, the extraction requires a positive scaling coordinate. If that coordinate vanishes, the same auxiliary solution may instead describe infeasibility or unboundedness. Ye, Todd, and Mizuno introduced a homogeneous self-dual linear program that can start from arbitrary positive primal and dual slack vectors, even when the original programs have no known feasible point (Ye–Todd–Mizuno 1994).

Their Theorem 3 concerns strictly self-complementary optimal solutions of the auxiliary program. Theorem 9 addresses a different question: under a regularity assumption on the original programs, does a general optimal solution of the auxiliary program still have a positive scaling coordinate? The distinction matters because optimality alone does not require every complementary pair to have a positive member. This mission formalizes the statement of Theorem 9 and the numbered identities that frame it.

Setting

Fix a real matrix $A\in\mathbb R^{m\times n}$ , a right-hand side $b\in\mathbb R^m$ , and a cost vector $c\in\mathbb R^n$ . The primal linear program (LP) minimizes $c^Tx$ subject to $Ax=b$ and $x\ge0$ . Its dual (LD) maximizes $b^Ty$ subject to $A^Ty\le c$ ; $y\in\mathbb R^m$ is unrestricted. The dual slack is $s=c-A^Ty$ .

An interior feasible point of (LP) is an $x$ with $Ax=b$ and every $x_j>0$ . An interior feasible point of (LD) is a $y$ with every component of $c-A^Ty$ positive. “Interior” here is the paper's strict coordinatewise feasibility condition, not the topological interior of an equality-constrained set in ambient space. The existence of such a point implies ordinary feasibility for the corresponding program.

The paper builds an auxiliary program (HLP) from initial vectors $x^0>0$ , $s^0>0$ , and $y^0$ . It uses the derived data

\bar b=b-Ax^0,\qquad \bar c=c-A^Ty^0-s^0,\qquad \bar z=c^Tx^0+1-b^Ty^0.

A point is a tuple $(y,x,\tau,\theta,s,\kappa)$ with $x,s,\tau,\kappa\ge0$ and free $y,\theta$ . Its equality constraints are

\begin{aligned} Ax-b\tau+\bar b\theta&=0,\\ s&=-A^Ty+c\tau-\bar c\theta,\\ \kappa&=b^Ty-c^Tx+\bar z\theta,\\ -\bar b^Ty+\bar c^Tx-\bar z\tau&=-(x^0)^Ts^0-1. \end{aligned}

The objective is to minimize $((x^0)^Ts^0+1)\theta$ . A feasible point is optimal when no feasible point has a smaller objective. The paper calls an optimal point self-complementary, whether or not its complementary pairs satisfy strict inequalities (p. 57, after Theorem 2(v)). After introducing the general construction, the paper fixes $y^0=0$ and $x^0=s^0=e$ , the all-ones vector. That is the instance used in Theorem 9.

Formalization targets

Goal: Theorem 9

If both (LP) and (LD) have interior feasible points, then every self-complementary solution $w^*=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ of this fixed (HLP) satisfies

\tau^*>0.

The theorem quantifies over every optimal point, including those that are not strictly self-complementary. The printed tuple writes $\theta^*=0$ ; Theorem 2(iv) entails that fact from optimality, so it is not an extra hypothesis in the goal (Theorem 9, p. 64).

Supporting targets

Theorem 2(iv) states that (HLP) has zero optimal value and, for every feasible point under arbitrary positive initial $x^0,s^0$ , satisfies

((x^0)^Ts^0+1)\theta=x^Ts+\tau\kappa.

Corollary 4 states that a positive $\kappa$ at an optimum under the fixed initialization entails infeasibility of (LP) or (LD). Equation (9) states the corresponding normalization identity

e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1.

These are separate milestone statements, each tied to its index and page in the paper (Theorem 2(iv), p. 57; equation (9), p. 58; Corollary 4, p. 59).

Significance

Theorem 9 says that the auxiliary model does not lose its positive scale at any optimum when the primal and dual programs are both strictly feasible. With $\tau^*>0$ , the homogeneous primal and dual variables can be divided by $\tau^*$ to recover solutions in the original scale. The result applies even when the auxiliary optimum lacks strict complementarity; that is the additional coverage beyond the strictly self-complementary case of Theorem 3 (Ye–Todd–Mizuno 1994, pp. 58 and 64).

The mathematical result was proved in 1994. This mission's remaining work is a machine-checked proof of the stated regularity result and its supporting claims in the paper's specific (HLP) model. The definitions of the homogeneous feasible set, its slacks, and its optimality relation are reusable for the other results in the same paper. The full algorithm and complexity estimate belong to the other missions in this series.

Difficulty

The optimality condition controls the objective, and Theorem 2(iv) identifies that objective with a sum of complementarity terms. Those facts alone permit $\tau^*=0$ ; they do not force the scaling coordinate to be positive. Theorem 3's assertion for a strictly self-complementary point cannot be applied to an arbitrary optimal point, because its strict support condition may fail. The challenge is to use interior feasibility of both original programs to exclude all zero-scale optima while retaining the full set of HLP optima in the quantifier.

Formalization scope

The Lean model uses finite-dimensional real vectors indexed by Fin m and Fin n, a real matrix $A$ , and a six-field HLP point in the paper's order $(y,x,\tau,\theta,s,\kappa)$ . The standard-form primal and dual feasible sets are reused from a published LP definition with the same minimization and maximization orientation. Paper-specific interior predicates and the homogeneous program are defined locally. Slack fields in an HLP point are constrained to equal their formulas, so they cannot be chosen independently to make a statement true.

The model first defines (HLP) for general $x^0,y^0,s^0$ and then substitutes the paper's choice (7). It treats self-complementarity as objective minimization over the whole feasible set. Defining it by $\theta=0$ or by a complementarity equation would erase the content of Theorem 2(iv). The objective and normalization constants are exact, including the $n+1$ in the fixed instance. No real supremum or infimum is used to define optimality; it is a direct comparison against every feasible point.

The dimensions $m,n$ may be zero. Empty coordinatewise inequalities then have their usual vacuous meaning, but the equations remain in force. In particular the prescribed point $(0,e,1,1,e,1)$ is strictly feasible for every $A,b,c$ , as a separate sorry-free local verification checks. This excludes an empty-feasible-set reading of the HLP definitions. Contributions proving the three numbered milestones, the goal, or reusable finite-dimensional LP lemmas are within scope.

Selected references

Yinyu Ye, Michael J. Todd, and Shinji Mizuno, An $O(\sqrt nL)$ -Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. DOI 10.1287/moor.19.1.53.

7 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Negative Dynamic Programming II: With Non-Positive Rewards on Borel Spaces, the Optimal Return Satisfies the Optimality EquationResearch Paper

Motivation

Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.

Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.

Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, $(p,\varepsilon)$ -optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation $J^* = T(J^*)$ under (P), (N) and (D).

Setting

The states $S$ and actions $A$ are non-empty Borel sets. A law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ . The return $r(s,a,t)$ is a Borel function with $-\infty < r \le 0$ whose expectation $\int r(s,a,t)\,dq(t\mid s,a)$ is finite for every $(s,a)$ . A policy $\pi = (\pi_1,\pi_2,\dots)$ draws the $n$ th action from a kernel $\pi_n(\cdot\mid s_1,a_1,\dots,s_n)$ that may depend on the whole history. A Markov policy $(f_1,f_2,\dots)$ uses measurable maps $f_n:S\to A$ , and a stationary policy $f^{(\infty)}$ uses one map at every stage. The expected return from the initial state $s$ is

I(\pi)(s) = \sum_{n\ge1} E^\pi_s\, r(s_n,a_n,s_{n+1}) \in [-\infty,0],

and the optimal return is

v^*(s) = \sup_\pi I(\pi)(s),

the supremum over all policies. Write $M(S)$ for the non-positive, extended real-valued Borel functions on $S$ . For $u\in M(S)$ and an action $a$ ,

T_a u(s) = \int \big[r(s,a,t) + u(t)\big]\,dq(t\mid s,a).

$T$ denotes the same operator for a measurable rule $f$ in place of $a$ , and $U = \sup_n T_n$ for a Markov policy $(f_1,f_2,\dots)$ . A policy $\pi^*$ is $(p,\varepsilon)$ -optimal, for a probability $p$ on $S$ , if $p\{I(\pi^*) \ge v^* - \varepsilon\} = 1$ . The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.

Formalization targets

Goal: the optimality equation (Theorem 8.2, negative case)

v^*(s) = \sup_{a\in A} T_a v^*(s) \qquad\text{for all } s\in S.

The equation involves no constants and no regularity hypotheses on $v^*$ .

Milestones

Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$ .
Theorem 6.1: if $Uv\ge v$ for $v\in M(S)$ , some Markov policy generated from $\hat\pi$ has $I(\pi)\ge v-\varepsilon$ .
Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$ .
Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
Lemma 7.1, Lemma 7.2: measurability of $(s,\nu)\mapsto\int u(s,x)\,d\nu(x)$ , and Borel measurability of the set of pairs $(s, e_\pi(s))$ , where $e_\pi(s)$ is the law of the future under $\pi$ .
Theorem 7.1: $v^*$ is absolutely measurable.
Theorem 8.1: for every $p$ and $\varepsilon>0$ a $(p,\varepsilon)$ -optimal Markov policy exists.

Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).

Significance

The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in $\sup_a T_a v^*$ can be tested for optimality. Value iteration and policy improvement can be compared with $v^*$ . The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case $v^*$ satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that $v^*$ is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.

Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.

Difficulty

Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state $t$ , a policy that is $\varepsilon$ -optimal from $t$ and concatenates. Without measurable selection this concatenation is not a policy. The set of $t$ where a given policy is $\varepsilon$ -optimal need not be Borel, and $v^*$ itself need not be Borel measurable, so even $\int v^*\,dq$ needs justification. Second, the contraction argument of the discounted case is unavailable. $U$ does not contract, it conserves $v+c$ along with $v$ , and value iteration from $0$ can converge to a function strictly above $v^*$ . The paper's Example 6.1 shows that the limit of $U^n0$ , the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.

Formalization scope

States and actions are non-empty standard Borel types. Policies are the published Blackwell plans (DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from $0$ (Lean's π.κ n is the paper's $\pi_{n+1}$ ). Markov policies are MarkovPlan; " $\pi$ -generated" and $G(\hat\pi)$ are the published IsGenerated and IsGeneratedPlan.
Only the negative case is formalized: $r\le0$ real-valued, $qr$ integrable, $\beta=1$ . The discounted and positive parts of Theorems 5.2, 7.1, 8.1 and 8.2, including the uniqueness and minimality clauses of Theorem 8.2, are not stated.
Returns take values in EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map $-\infty$ to $0$ and make the goal false or vacuous.
$v^*$ is the supremum over all plans. It is not assumed measurable and is never replaced by a measurable modification. $T_a v^*$ is a lintegral of a possibly non-measurable function, which equals the completion integral because $v^*$ is absolutely measurable (Theorem 7.1).
Explicit readings of the page: the hypothesis $u\in M(S)$ of each operator statement is IsNegM u. Theorem 5.2(b) assumes $u+c\in M(S)$ . " $U$ conserves $v$ " includes $v\in M(S)$ . Lemma 6.2 asserts that the limit defining $v_\pi$ exists. Theorem 6.2 states $\ge$ everywhere and $>$ where $\sup_j I(\pi^j) > -\infty$ (the printed $>$ fails where the supremum is $-\infty$ ). $(p,\varepsilon)$ -optimality is " $p$ -almost everywhere". Absolute measurability is NullMeasurable for every probability measure. $P(X)$ carries the Giry σ-field. The extra Theorem 8.4 reads the printed " $I(\pi) < u$ " as " $\le$ " (the strict reading is false).
Reusable infrastructure: the negative model, the Ionescu-Tulcea law of the future (futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell, Positive Dynamic Programming, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
L. E. Dubins and L. J. Savage, How to Gamble If You Must, McGraw-Hill, 1965.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

21 thms2 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research III: Minimum Average Journey Time on Alternative Routes — Equal Marginal Times ε and the Closed Forms (32)–(33)Research Paper

Motivation

J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259) introduced the two criteria that still organise traffic assignment. When a flow of traffic can choose between several routes from one origin to one destination, the paper (p. 345) considers two ways the traffic might divide:

the journey times on all the routes actually used are equal, and less than those that a single vehicle would experience on any unused route;
the average journey time is a minimum.

The first is now called Wardrop's first principle, or user equilibrium: no driver can shorten their trip by switching route. The second, Wardrop's second principle, is the system optimum: it "minimizes the vehicle-hours spent on the journey". The gap between the two is the quantity later studied as the price of anarchy of selfish routing (Roughgarden and Tardos, J. ACM 2002), and the marginal-cost characterisation of the system optimum underlies congestion pricing (Beckmann, McGuire and Winsten, Studies in the Economics of Transportation, 1956).

This mission formalizes the paper's solution of criterion (2) on parallel routes, section (2) Minimum Average Time, pp. 345–347. Mission II of the same series treats criterion (1) on the same model.

Setting

A total additional flow $Q$ is divided among $D$ alternative routes $i = 1, \dots, D$ . Route $i$ carries an additional flow $q_i$ and has journey time, equation (22),

t_i(q_i) = \frac{b_i}{1 - q_i/p_i},

where $b_i > 0$ is the journey time on route $i$ with no additional flow and $p_i > 0$ is the additional flow at which its speed would fall to zero (routeTime b p i x). A feasible split of $Q$ is a vector $q$ with $0 \le q_i < p_i$ for every $i$ and $\sum_i q_i = Q$ (IsFeasible p Q q).

The number of additional vehicles on route $i$ at an instant is $z_i = q_i t_i$ , and $Z = \sum_i z_i$ (totalExtra b p q). The average journey time is, equations (25)–(26),

T = \sum_{i=1}^D \frac{q_i t_i}{Q} = \frac{Z}{Q}

(avgTime b p Q q). Criterion (2) asks for a feasible split $q$ with $T(q) \le T(z)$ for every feasible split $z$ (IsMinAvgTime b p Q q).

The marginal journey time of route $i$ is $d(q_i t_i)/dq_i$ , the rate at which $Z$ grows when flow is added to that route. For a threshold $\varepsilon$ , $U(\varepsilon) = \{i : b_i < \varepsilon\}$ (usedSet b ε) is the set of routes whose marginal time at zero flow lies below $\varepsilon$ ; with the routes labelled so that $b_1 < \dots < b_D$ it is the paper's "first $j$ routes".

Formalization targets

Goal: the closed forms (32)–(33)

For $b_i, p_i > 0$ and $0 < Q < \sum_i p_i$ , every split $q$ minimizing $T$ admits a threshold $\varepsilon > 0$ with $\sum_{i \in U} p_i > Q$ , where $U = U(\varepsilon)$ , such that

q_h = \begin{cases} p_h\left\{1 - \dfrac{\left(\sum_{i\in U} p_i - Q\right)\sqrt{b_h}}{\sum_{i\in U} p_i\sqrt{b_i}}\right\}, & b_h < \varepsilon,\\[1ex] 0, & \text{otherwise,}\end{cases} \qquad T = \frac1Q\left\{\frac{\left(\sum_{i\in U} p_i\sqrt{b_i}\right)^2}{\sum_{i\in U} p_i - Q} - \sum_{i\in U} p_i b_i\right\}.

Milestones

(29)–(30): $d(q_i t_i)/dq_i = b_i/(1 - q_i/p_i)^2$ , equal to $b_i$ at $q_i = 0$ .
(27)–(28): at a minimum, all routes in use have the same marginal time $\varepsilon$ .
A route $j$ with $b_j \ge \varepsilon$ is not used.
The routes in use are exactly those with $b_i < \varepsilon$ , and on them $1 - q_i/p_i = \sqrt{b_i/\varepsilon}$ .
(31): $\sum_{i\in U} p_i - Q = \sum_{i\in U} p_i\sqrt{b_i/\varepsilon}$ .

A companion theorem states that a minimizing split exists whenever $0 < Q < \sum_i p_i$ .

Significance

The closed forms give the system-optimal assignment on parallel routes with the travel-time law (22) explicitly: which routes carry traffic, how much, and the resulting average time. Together with the equal-times solution (23)–(24) of mission II they quantify, for this model, how much average time selfish route choice costs; the paper's Fig. 8 compares the two numerically and finds the difference small in its example. The marginal-time conditions (27)–(28) are the parallel-route instance of the general statement that a system optimum is an equilibrium with respect to marginal costs.

The derivation on pp. 346–347 is a first-order argument that the paper does not make rigorous: it assumes a minimizer exists, that it satisfies the stationarity condition, and leaves (32)–(33) to "a few lines of algebra". This mission produces the rigorous version, including existence. No machine-checked statement of (27)–(33) is on the platform; the related platform items on Wardrop equilibria concern the Beckmann potential and atomic congestion games, not the system optimum of this model.

Difficulty

The stationarity condition (27) comes from moving an infinitesimal flow between two routes in use. Turning this into a theorem needs the one-sided version at unused routes, since $q_j = 0$ is a boundary point and the condition there is an inequality, and needs the constraint $\sum_i q_i = Q$ to be preserved by the perturbation. The step "only the first $j$ routes will be in use" is the converse direction: a route with $b_i < \varepsilon$ that carries no flow must be shown to contradict minimality, not just to violate the equal-marginals equation.

Existence is not a compactness argument on a closed set: the feasible set is open in the direction $q_i \to p_i$ , where $q_i t_i \to \infty$ , and that coercivity has to be used. The algebra from (31) to (32)–(33) is routine once the set $U$ and the value of $\varepsilon$ are fixed.

Formalization scope

Routes are indexed by Fin D; all quantities are real. The standing hypotheses are $b_i > 0$ , $p_i > 0$ , $0 < Q$ and $Q < \sum_i p_i$ ; without the last the feasible set is empty and every statement about a minimizer is vacuous, and with $Q \le 0$ the average time $Z/Q$ is undefined. Feasibility requires $q_i < p_i$ , of the minimizer and of every competitor: at $q_i = p_i$ Lean evaluates $b_i/0$ as $0$ , which would let a "minimizer" place flow at capacity for free. The paper's labelling $b_1 < \dots < b_D$ is not assumed; "the first $j$ routes" is $U(\varepsilon)$ . Marginal times are written in the closed form (29), and milestone 1 identifies that form with the derivative via HasDerivAt. Minimality is stated for $T$ , the paper's criterion, not for $Z$ .

Corrected slip. The paper prints the denominator of (33) as $\sum_{i=1}^j p_i b_i$ . The formalization uses $\sum_{i=1}^j p_i\sqrt{b_i}$ : from (31), $1/\sqrt\varepsilon = (\sum p_i - Q)/\sum p_i\sqrt{b_i}$ , and $q_h = p_h(1 - \sqrt{b_h/\varepsilon})$ . The printed form is not dimensionally consistent and gives wrong flows, e.g. for $b = (4, 9)$ , $p = (10, 10)$ , $Q = 35/3$ . Equation (32) is correct as printed.

The goal cannot be satisfied trivially: the threshold $\varepsilon$ is existential and the flows and $T$ are pinned to explicit formulas, and the companion existence theorem shows the hypothesis IsMinAvgTime is met for every admissible $Q$ . The route time and feasible split come from the shared WardropTraffic.EqualTimes.Setting definition; this mission adds the total and average time and criterion (2). Proofs of any item, including the existence theorem and a uniqueness statement (the objective is strictly convex), are welcome.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Instn Civ. Engrs Part II 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
T. Roughgarden, É. Tardos, How bad is selfish routing?, J. ACM 49(2) (2002), 236–259. https://doi.org/10.1145/506147.506153

8 thms2 active usersReviewed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Fast Approximation Algorithms for Fractional Packing and Covering Problems 2: An ε-Relaxed Decision Procedure for Fractional Covering Using O(m + ρ log² m + ε⁻²ρ log(m/ε)) Oracle CallsResearch Paper

Motivation

Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form $Ax\ge b$ with $A\ge 0$ : the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).

The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).

Setting

Fix integers $m\ge1$ , $n$ . Let $A$ be a real $m\times n$ matrix with nonnegative entries and rows $a_1,\dots,a_m$ , write $a_ix=\sum_j A_{ij}x_j$ , let $b\in\mathbb R^m$ with $b>0$ , and let $P\subseteq\mathbb R^n$ be a nonempty convex set contained in the nonnegative orthant.

COVERING asks whether there is $x\in P$ with $Ax\ge b$ ; such an $x$ is an exact solution. For $\varepsilon>0$ , an $\varepsilon$ -approximate solution is $x\in P$ with $Ax\ge(1-\varepsilon)b$ .
For $x\in\mathbb R^n$ , $\lambda(x)=\min_i a_ix/b_i$ is the largest $\lambda$ with $Ax\ge\lambda b$ , and $\lambda^*=\max\{\lambda(x):x\in P\}$ . A point $x\in P$ is $\varepsilon$ -optimal when $\lambda(x)\ge(1-\varepsilon)\lambda^*$ .
The width is $\max_i\max_{x\in P}a_ix/b_i$ ; a number $\rho>0$ with $a_ix\le\rho\,b_i$ for all $x\in P$ and all $i$ is a width bound.
Subroutine (7) receives $y\in\mathbb R^m$ , $y\ge0$ , and returns $\tilde x\in P$ maximizing $y^tAx$ over $P$ ; $C_{\mathcal C}(y)$ is that maximum.
For $\alpha>0$ , the dual solution corresponding to $x$ is $y_i=\frac1{b_i}e^{-\alpha a_ix/b_i}$ , and the potential is $\Phi=y^tb=\sum_ie^{-\alpha a_ix/b_i}$ .
The relaxed optimality conditions are $(\mathcal C1)$ : $(1+\varepsilon)\lambda\,y^tb\ge y^tAx$ , and $(\mathcal C2)$ : $C_{\mathcal C}(y)-y^tAx\le\varepsilon\,(C_{\mathcal C}(y)+y^tb)$ .
IMPROVE-COVER $(x,\varepsilon)$ (Figure 3) sets $\lambda_0=\lambda(x)$ , $\alpha=4\lambda_0^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ and $\sigma=\varepsilon/(4\alpha\rho)$ ; while $\lambda(x)\le2\lambda_0$ and $\mathcal C2$ fails, it moves $x$ to $(1-\sigma)x+\sigma\tilde x$ , $\tilde x$ the subroutine's answer for the current dual solution.
The covering algorithm obtains a start with $Ax\ge\frac1mb$ from $m$ subroutine calls, calls IMPROVE-COVER with $\varepsilon=1/6$ until $\mathcal C2$ holds or an exact solution appears, then halves $\varepsilon$ phase by phase.

The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.

Formalization targets

Goal: Theorem 3.7 (p. 21)

For every instance as above, every width bound $\rho$ , every exact maximization oracle and every $0<\varepsilon_0<1$ , the covering algorithm stops after at most

N=m+\big(\lceil\log_2m\rceil+1\big)\big(2+4320\,\rho\ln(24m)\big)+2\lceil\log_2\varepsilon_0^{-1}\rceil+9408\,\rho\,\varepsilon_0^{-2}\ln\frac{24m}{\varepsilon_0}

calls to subroutine (7), and either returns $x\in P$ with $Ax\ge(1-\varepsilon_0)b$ , or reports that no $x\in P$ has $Ax\ge b$ , correctly. This is the paper's $O(m+\rho\log^2m+\varepsilon^{-2}\rho\log(m\varepsilon^{-1}))$ with the constants of its proof.

Milestones

In the order the proof uses them:

Lemma 3.1: $\mathcal C1$ and $\mathcal C2$ imply that no exact solution exists if $\lambda\le1-3\varepsilon$ , and that $x$ is $3\varepsilon$ -optimal if $\lambda\ge1-3\varepsilon$ .
Lemma 3.2: if $\alpha\ge2\lambda^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ , the dual solution corresponding to $x$ satisfies $\mathcal C1$ .
Lemma 3.3: while $\mathcal C2$ fails, a step of size $\sigma\le\varepsilon/(4\alpha\rho)$ lowers the potential: $\Phi-\hat\Phi\ge\varepsilon\alpha\sigma\Phi$ .
Lemma 3.4: during IMPROVE-COVER, $\lambda\ge\frac34\lambda_0$ .
Theorem 3.5: one call of IMPROVE-COVER makes at most $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ oracle calls, and at most $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ from a $6\varepsilon$ -optimal start with $\varepsilon\le1/12$ .
Lemma 3.6: $m$ oracle calls give $x\in P$ with $Ax\ge\frac1mb$ , or prove that no exact solution exists.

Significance

Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about $\rho\varepsilon^{-2}\log(m/\varepsilon)$ linear optimizations over $P$ , plus lower-order terms in $m$ . In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where $P$ is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.

The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.

Difficulty

The obvious argument tracks the potential $\Phi$ and stops when it is small. This does not work directly, because $\alpha$ is tied to $\lambda_0$ , and the guarantee $\mathcal C1$ depends on $\lambda$ staying close to $\lambda_0$ throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition $\mathcal C2$ is not scaled by $\lambda$ , so $\mathcal C1$ and $\mathcal C2$ give $\varepsilon$ -optimality only when $\lambda$ is near $1$ ; the first phase must first raise $\lambda$ from $1/m$ by repeated doubling. And the cost of $\varepsilon$ -scaling is bounded only because each phase starts from a $6\varepsilon$ -optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit $N$ , over a fuel-bounded run, is substantial.

Formalization scope

Rows are Fin m with [NeZero m], coordinates Fin n; $A$ is a Matrix (Fin m) (Fin n) ℝ; $P$ is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. $\lambda(x)$ is a Finset.inf' over the rows. Conventions committed to:

Width. $\rho$ is any upper bound with $\rho>0$ , not a supremum; the theorems hold for every such bound, the exact width included.
Oracle. Subroutine (7) is a function that, for every $y\ge0$ , returns a maximizer of $y^tAx$ over $P$ ; every theorem quantifies over all such functions. Box (7) of the report prints "min", but every use maximizes; the maximizer reading is adopted.
Optimality without $\lambda^*$ . " $x$ is $c\varepsilon$ -optimal" is stated as $(1-c\varepsilon)\lambda(x')\le\lambda(x)$ for every $x'\in P$ .
Runs. IMPROVE-COVER and the driver are fuel-bounded functions returning some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the $\mathcal C2$ check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel $\lceil N\rceil$ stops; it does not assume termination.
Driver. The prose of pp. 20–21 is written down as initCover, firstPhase and scalingPhases with $\varepsilon_k=\frac16 2^{-k}$ .
Constants replacing $O(\cdot)$ . Theorem 3.5: $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ and $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ oracle calls. Theorem 3.7: the $N$ above.
Implicit hypotheses made explicit. $y\ne0$ and $\varepsilon<\frac13$ in Lemma 3.1; $\lambda>0$ in Lemmas 3.2–3.4 and Theorem 3.5; $\sigma\ge0$ in Lemma 3.3.
Misprint. Theorem 3.5's second sentence names IMPROVE-PACKING; it is stated for IMPROVE-COVER.

A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.

A complete development needs elementary real analysis (the second-order bound $e^{x+\delta}\le e^x+\delta e^x+\frac\varepsilon2|\delta|e^x$ for $|\delta|\le\varepsilon/4$ ), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.

Selected references

S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Cornell University School of ORIE Technical Report No. 999, February 1992. https://core.ac.uk/download/79020349.pdf
S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Mathematics of Operations Research 20(2), 257–301, 1995. https://doi.org/10.1287/moor.20.2.257
N. Garg, J. Könemann, Faster and Simpler Algorithms for Multicommodity Flow and Other Fractional Packing Problems, SIAM Journal on Computing 37(2), 630–652, 2007. https://doi.org/10.1137/S0097539704446232
N. E. Young, Sequential and Parallel Algorithms for Mixed Packing and Covering, Proc. 42nd IEEE FOCS, 538–546, 2001. https://arxiv.org/abs/cs/0110040

10 thms2 active usersReviewed

Convex Optimization Operations Research·Captain: mikedeng1

A Dual Approach to Solving Nonlinear Programming Problems by Unconstrained Optimization 2: For a Normal Convex Program and Any Dual Optimal ȳ, x̄ Is Optimal iff x̄ Minimizes L_r(·, ȳ)Research Paper

Motivation

Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector $\bar y$ exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal $\bar y$ does not tell where the primal optimum is, because the minimizers of $x \mapsto L_0(x, \bar y)$ over $X$ typically include points that are not optimal and not even feasible. A linear program is the extreme case: $L_0(\cdot, \bar y)$ is then often constant.

The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for $r > 0$ , minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for $L_0$ has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.

Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian $L_r$ below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.

Setting

Let $E$ be a real vector space, $X \subseteq E$ a nonempty convex set, and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex functions. The problem is

\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \quad\text{subject to } f_i(x) \le 0,\ i = 1, \dots, m.

A point is feasible if it lies in $X$ and satisfies the constraints. The optimal value "inf in (P)" is the infimum of $f_0$ over the feasible points, an element of $[-\infty, +\infty]$ . An optimal solution is a feasible $\bar x$ with $f_0(\bar x) \le f_0(x)$ for every feasible $x$ .

For $y \in \mathbb R^m$ (no sign restriction), $\theta(t) = \max\{0, t\}$ and $r > 0$ , the penalty Lagrangian is

L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big].

The ordinary Lagrangian is $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$ for $y \ge 0$ , and $-\infty$ otherwise. The dual objectives are $g_r(y) = \inf_{x \in X} L_r(x, y)$ and $g_0(y) = \inf_{x \in X} L_0(x, y)$ . Problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$ .

A dual optimal solution is a maximizer $\bar y$ of $g_r$ with $g_r(\bar y) > -\infty$ .
(P) is normal if the dual optimal value $\sup g_0$ equals the optimal value of (P).
$\bar y$ is a Kuhn–Tucker vector relative to $L_r$ if $-\infty < \inf_{x \in X} L_r(x, \bar y) = \inf$ in (P).
$(\bar x, \bar y)$ is a saddle point of $L_r$ if $\bar x \in X$ and $L_r(\bar x, y) \le L_r(\bar x, \bar y) \le L_r(x, \bar y)$ for all $x \in X$ , $y \in \mathbb R^m$ .

In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.

Formalization targets

Goal: Theorem 3.5 (p. 362)

Assume (P) is normal, $\bar y$ is a dual optimal solution, and $r > 0$ . Then for every $\bar x \in E$

\bar x \text{ is optimal for (P)} \iff \bar x \in X \text{ and } L_r(\bar x, \bar y) \le L_r(x, \bar y) \ \ \forall x \in X.

Milestones (attack order)

§3 after (3.17), pp. 361–362: for $r > 0$ , $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ iff $\bar y$ is optimal for $(D_r)$ and (P) is normal.
§3, p. 362: for $r > 0$ , $(\bar x, \bar y)$ is a saddle point of $L_r$ iff $\bar x$ is optimal for (P) and $\bar y$ is a Kuhn–Tucker vector.
Corollary 3.4, $r > 0$ (p. 362): $L_r$ and $L_0$ have the same Kuhn–Tucker vectors and the same saddle points, and the saddle points of $L_r$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions

\bar y_i \ge 0,\ f_i(\bar x) \le 0,\ \bar y_i f_i(\bar x) = 0\ (\forall i), \qquad \bar x \in \operatorname{argmin}_X \Big(f_0 + \sum_i \bar y_i f_i\Big).

Corollary 3.4, $r = 0$ : the saddle points of $L_0$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions.
Proof of Theorem 3.5, pp. 362–363: if $\bar y$ is optimal for $(D_r)$ and $\bar x \in X$ minimizes $L_r(\cdot, \bar y)$ over $X$ , then $\nabla_y L_r(\bar x, \bar y) = 0$ and $\bar y$ maximizes $L_r(\bar x, \cdot)$ over $\mathbb R^m$ .

Significance

The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of $L_r(\cdot, \bar y)$ over $X$ solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function $g_r$ over $\mathbb R^m$ , then minimize $L_r(\cdot, \bar y)$ over $X$ . For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, $L_r$ behaves exactly like $L_0$ .

Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on $\mathbb R^n$ (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.

Difficulty

The "if" direction is the substantive one. A minimizer $\bar x$ of $L_r(\cdot, \bar y)$ is not known to be feasible; feasibility must come from maximality of $\bar y$ in the dual. The natural argument for $L_0$ breaks at exactly this point: $L_0(\bar x, \cdot)$ is affine on the orthant, and minimality in $x$ gives no information about $\nabla_y$ . For $L_r$ the link is the differentiability of the dual function $g_r$ with $\nabla g_r(\bar y) = \nabla_y L_r(\bar x, \bar y)$ (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so $\pm\infty$ must be handled at each step.

Formalization scope

$E$ is a bare real vector space (AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.
$X$ is a Set E. Each statement assumes the paper's standing hypothesis (p. 358): $X$ convex and nonempty, $f_0, \dots, f_m$ convex on $X$ .
The $f_i$ are total functions E → ℝ, and only their values on $X$ enter. Constraint indices are Fin m (0-based), with $f_0$ a separate argument.
$\mathbb R^m$ is EuclideanSpace ℝ (Fin m).
$g_r$ , $g_0$ , $L_0$ , the optimal value of (P) and the dual optimal value are EReal-valued. An infeasible (P) has value $+\infty$ , and $g_0 = -\infty$ off $y \ge 0$ .
$r > 0$ is an explicit hypothesis wherever the paper has it. Theorem 3.5 is false for $r = 0$ (p. 363), and the Lean expression Lr at $r = 0$ is not $L_0$ .
"Dual optimal solution" in Theorem 3.5 is read as optimal for $(D_r)$ with the same $r$ , with $g_r(\bar y) > -\infty$ (the convention of p. 361). The paper's reading, optimal for $(D_0)$ , is equivalent by Theorem 3.2, which is posed in mission 1 of this series.
" $\bar x$ minimizes $L_r(\cdot, \bar y)$ over $X$ " includes $\bar x \in X$ . The equivalence is stated for every $\bar x \in E$ . No sign condition is imposed on $\bar y$ : nonnegativity is a consequence of dual optimality, not a hypothesis.
Saddle points are taken over $X \times \mathbb R^m$ (Rockafellar's Convex Analysis, §36). For $L_0$ they are taken in the extended reals.
Trivializing readings ruled out: normality is neither dropped nor replaced by existence of an optimal solution or by Slater's condition, and the minimization on the right of Theorem 3.5 is never over a set containing points outside $X$ .

The solver needs the representation $L_r(x, y) = \min_u\{F_r(x, u) + u \cdot y\}$ , weak duality, the envelope formula and differentiability of $g_r$ (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.

Selected references

R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.

8 thms2 active usersReviewed

Completed

Convex Optimization·Captain: mikedeng1

A D.C. Optimization Algorithm for Solving the Trust-Region Subproblem I: A Point x Solves the D.C. Program min(g − h) if and only if ∂_εh(x) ⊂ ∂_εg(x) for Every ε > 0Research Paper

Motivation

A d.c. program minimizes a difference of two convex functions. Many nonconvex problems of practical interest have this form: every function with a locally Lipschitz gradient on $\mathbb R^n$ is d.c., the class is closed under finite sums, products and finite suprema, and constrained problems enter through indicator functions. Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) use this structure to build the DCA, an algorithm for the trust-region subproblem $\min\{\tfrac12 x^\top Ax+b^\top x:\|x\|\le r\}$ , a basic step of trust-region methods in nonlinear optimization. The algorithm rests on a duality theory for d.c. programs, which §3.1 of the paper sets out. This mission is the global half of that theory.

Timeline.

1978–1979: J. F. Toland introduces the duality $\inf(g-h)=\inf(h^*-g^*)$ and the inclusions between primal and dual solution sets, in a general setting of linear spaces in separating duality (J. Math. Anal. Appl. 66 (1978); Bull. Soc. Math. France, Mémoire 60 (1979), pp. 177–183, numdam).
1988: J.-B. Hiriart-Urruty proves that $x$ minimizes $g-h$ if and only if $\partial_\varepsilon h(x)\subset\partial_\varepsilon g(x)$ for every $\varepsilon>0$ , through the behaviour of the $\varepsilon$ -directional derivative as a function of $\varepsilon$ (From convex optimization to non convex optimization. Part I, in Nonsmooth Optimization and Related Topics, Plenum, 1988; reference [9] of the paper). The same year Pham Dinh and Elbernoussi introduce the DCA on the basis of d.c. duality (reference [23]).
1998: Pham Dinh and Le Thi give a short proof of Hiriart-Urruty's condition through the d.c. duality (Theorem 3.1, p. 483) and use the duality to design and analyse the DCA for the trust-region subproblem.

Setting

Let $X=\mathbb R^n$ with its canonical inner product $\langle\cdot,\cdot\rangle$ , and identify the dual space $Y$ with $X$ . Functions take values in $\mathbb R\cup\{+\infty\}$ . A function $\theta$ is in $\Gamma_0(X)$ if it is convex, lower semicontinuous, never $-\infty$ , and finite at some point. Its effective domain is $\operatorname{dom}\theta=\{x:\theta(x)<+\infty\}$ , and its conjugate is

\theta^*(y)=\sup\{\langle x,y\rangle-\theta(x):x\in X\}.

For $x_0\in\operatorname{dom}\theta$ , the subdifferential $\partial\theta(x_0)$ is the set of $y$ with $\theta(x)\ge\theta(x_0)+\langle x-x_0,y\rangle$ for all $x$ . For $\varepsilon>0$ the $\varepsilon$ -subdifferential is

\partial_\varepsilon\theta(x_0)=\{y\in Y:\theta(x)\ge\theta(x_0)+\langle x-x_0,y\rangle-\varepsilon\ \ \forall x\in X\}.

Given $g,h\in\Gamma_0(X)$ , the d.c. program and its dual are

\text{(P)}\quad\alpha=\inf\{g(x)-h(x):x\in X\},\qquad \text{(D)}\quad\alpha=\inf\{h^*(y)-g^*(y):y\in Y\},

with the convention $+\infty-(+\infty)=+\infty$ . Throughout, the paper assumes the inclusions

\operatorname{dom}g\subset\operatorname{dom}h,\qquad\operatorname{dom}h^*\subset\operatorname{dom}g^*.\tag{3}

$\mathcal P$ and $\mathcal D$ denote the solution sets of (P) and (D).

Formalization targets

Goal: Theorem 3.1(i), p. 483

For every $x\in\operatorname{dom}h$ ,

x\in\mathcal P\iff\partial_\varepsilon h(x)\subset\partial_\varepsilon g(x)\quad\forall\varepsilon>0.

Milestones (the proof on pp. 483–484)

d.c. duality (§3, pp. 481–482): $\inf\{g-h\}=\inf\{h^*-g^*\}$ .
(6)–(7) (p. 483): $x^*\in\mathcal P$ iff $x^*\in\operatorname{dom}g$ and $g(x^*)+g^*(y)\le h(x^*)+h^*(y)$ for all $y\in\operatorname{dom}h^*$ .
(8) (p. 484): for $x^*\in\operatorname{dom}h$ , the inclusions $\partial_\varepsilon h(x^*)\subset\partial_\varepsilon g(x^*)$ for all $\varepsilon>0$ are equivalent to $\langle x^*,y\rangle+\varepsilon\ge h(x^*)+h^*(y)\Rightarrow\langle x^*,y\rangle+\varepsilon\ge g(x^*)+g^*(y)$ for all $\varepsilon>0$ and $y$ .
(7) ⇔ (8) (p. 484), for $x^*\in\operatorname{dom}h$ .

Companions

Theorem 3.1(ii): for $y\in\operatorname{dom}g^*$ , $y\in\mathcal D\iff\partial_\varepsilon g^*(y)\subset\partial_\varepsilon h^*(y)$ for all $\varepsilon>0$ .
Theorem 3.1(iii): $\bigcup\{\partial h(x):x\in\mathcal P\}\subset\mathcal D\subset\operatorname{dom}h^*$ , with equality in the first inclusion when $g^*$ is subdifferentiable on $\mathcal D$ .
Theorem 3.1(iv): $\bigcup\{\partial g^*(y):y\in\mathcal D\}\subset\mathcal P\subset\operatorname{dom}g$ , with equality when $h$ is subdifferentiable on $\mathcal P$ .

Significance

The result. Theorem 3.1(i) characterizes global minimizers of a nonconvex function by inclusions between convex objects. It is a certificate of global optimality that uses only convex analysis. Parts (iii) and (iv) say that a solution of either program yields a solution of the other through a subgradient. This is the mechanism of the DCA, which alternates $y^k\in\partial h(x^k)$ , $x^{k+1}\in\partial g^*(y^k)$ . The paper notes that condition (i) is hard to use in an algorithm and that the DCA rests on local conditions instead. The global condition remains the reference statement that the local theory and the DCA approximate.

Formalizing it. All results here are classical and proved on paper. Parts (iii) and (iv) are proved in references the paper cites, not in the paper itself. None of them has a machine-checked proof on the platform. The mission provides a Lean layer for d.c. programming on $\mathbb R^n$ : the convention-respecting difference, the $\varepsilon$ -subdifferential, the standing assumptions, and the primal and dual solution sets. Missions II and III of the series reuse this layer for local optimality and for the convergence of the DCA.

Difficulty

The paper's proof is short, but each step uses a fact that needs separate work. The duality requires the biconjugation $h=h^{**}$ for $h\in\Gamma_0$ , and an exchange of two infima in the extended reals under the convention $+\infty-(+\infty)=+\infty$ . The step (7) ⇔ (8) has a hidden case: a point of $\operatorname{dom}h\setminus\operatorname{dom}g$ . Ruling it out needs $\partial_\varepsilon h(x^*)\neq\emptyset$ for $\varepsilon>0$ , a nontrivial property of lower semicontinuous proper convex functions. The obvious approach, computing with real numbers, fails because $g$ , $h$ , $g^*$ and $h^*$ all take the value $+\infty$ , and the extended-real arithmetic of Lean does not follow the paper's convention.

Formalization scope

Space. $X=Y$ is EuclideanSpace ℝ (Fin n). Functions are EReal-valued.
Published definitions. $\Gamma_0$ is ThreeOpSplitting.ConvexRates.IsProperClosedConvex, $\partial$ is InertialFB.IFB.IsSubgradient, and the conjugate is CondatPD.FinDim.conj, an extended-real supremum over all of $X$ .
Convention. Mathlib has $\top-\top=\bot$ . Every difference $g-h$ and $h^*-g^*$ of the paper is the explicit dcSub, which returns $+\infty$ when the first term is $+\infty$ . $\mathcal P$ , $\mathcal D$ and $\alpha$ are defined through it.
Domains. The $\varepsilon$ -subdifferential is empty outside the domain, as in the paper's definition. Theorem 3.1(i) is stated for $x\in\operatorname{dom}h$ , the case its proof treats. For $x\notin\operatorname{dom}h$ the right-hand side holds vacuously while $x\notin\mathcal P$ . Every solution lies in $\operatorname{dom}g\subset\operatorname{dom}h$ , and for $x\in\operatorname{dom}h\setminus\operatorname{dom}g$ both sides are false, so the restriction loses nothing. Part (ii) is restricted to $y\in\operatorname{dom}g^*$ for the same reason.
Standing assumptions. $g,h\in\Gamma_0$ and the inclusions (3) are a hypothesis of every item. Finiteness of $\alpha$ is not assumed: when $\alpha=-\infty$ , both solution sets are empty.
Not a trivialization. Defining the $\varepsilon$ -subdifferential without the domain clause, or using Mathlib's subtraction for $g-h$ , would change the theorem: the first makes every $y$ an $\varepsilon$ -subgradient at points where the function is $+\infty$ , and the second sets $g-h=-\infty$ wherever $g$ and $h$ are both $+\infty$ , since Lean's $\top-\top=\bot$ . The goal does not mention (6), (7), (8) or the duality.
Parts (iii) and (iv) include the paper's "in particular" sufficient conditions, with the relative interior written as Mathlib's intrinsicInterior, and the "in this case" inclusions into $\operatorname{dom}\partial g^*\cap\operatorname{dom}\partial h^*$ and $\operatorname{dom}\partial g\cap\operatorname{dom}\partial h$ .
Contributions welcome. Biconjugation and Fenchel–Young for EReal-valued functions on EuclideanSpace in the conventions of CondatPD.FinDim.conj, nonemptiness of $\varepsilon$ -subdifferentials, and the extended-real infimum exchange. These are reusable well beyond d.c. programming.

Selected references

Pham Dinh Tao and Le Thi Hoai An, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM J. Optim. 8(2):476–505, 1998. https://doi.org/10.1137/S1052623494274313
J. F. Toland, Duality in nonconvex optimization, J. Math. Anal. Appl. 66:399–415, 1978. https://doi.org/10.1016/0022-247X(78)90243-3
J. F. Toland, On subdifferential calculus and duality in nonconvex optimization, Bull. Soc. Math. France, Mémoire 60:177–183, 1979. http://www.numdam.org/item/MSMF_1979__60__177_0/
J.-B. Hiriart-Urruty, From convex optimization to non convex optimization. Part I: Necessary and sufficient conditions for global optimality, in Nonsmooth Optimization and Related Topics, Ettore Majorana Internat. Sci. Ser. Phys. Sci. 43, Plenum Press, New York, 1988 (no persistent link; cited as [9] in the paper above).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

9 thms2 active usersReviewed

Convex Optimization Numerical Analysis Operations Research·Captain: mikedeng1

Fixed Point and Bregman Iterative Methods for Matrix Rank Minimization: The Matrix Shrinkage Fixed Point Iteration Converges to an Optimal Solution of the Nuclear Norm Regularized ProblemResearch Paper

Motivation

Many estimation problems ask for a matrix of low rank that is consistent with a small number of linear measurements: completing a partially observed ratings matrix, identifying a low-order linear system, or embedding points from a few pairwise distances. Rank minimization under linear constraints is NP-hard, and the standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values (Recht, Fazel and Parrilo, 2010). Under incoherence assumptions the surrogate recovers the low-rank matrix exactly (Candès and Recht, 2009).

The surrogate is a semidefinite program, and interior point methods for it do not scale past matrices of a few hundred rows. Ma, Goldfarb and Chen (2009) proposed a first-order method for the regularized form of the problem: a gradient step on the data-fit term followed by singular value shrinkage. Their algorithms FPC and FPCA are built on this two-line iteration, and the paper's one convergence theorem says that the iteration, run with a fixed step size, converges to a minimizer. This mission formalizes that theorem and the lemmas used to prove it.

Timeline of the closest results:

2005: Combettes and Wajs prove convergence of forward–backward splitting for the sum of a convex function and a convex function with Lipschitz gradient in a Hilbert space.
2008: Hale, Yin and Zhang analyse the fixed point continuation (FPC) method for $\ell_1$ -regularized least squares, with vector shrinkage in place of matrix shrinkage.
2008–2010: Cai, Candès and Shen introduce singular value thresholding (SVT) for matrix completion, prove that the shrinkage is the proximal map of the nuclear norm, and prove convergence of a different iteration (Uzawa's method on a strongly convex problem with equality constraints).
2009: Ma, Goldfarb and Chen state and prove convergence of the matrix shrinkage fixed point iteration for the nuclear norm regularized least squares problem (1.8), following Hale, Yin and Zhang's argument.

Setting

Fix natural numbers $m,n,p$ . Matrices $X\in\mathbb R^{m\times n}$ carry the Frobenius norm $\|X\|_F=(\sum_{ij}X_{ij}^2)^{1/2}$ and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$ . A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by matrices $A_0,\dots,A_{p-1}$ through $\mathcal A(X)_i=\langle A_i,X\rangle$ ; equivalently $\mathcal AX=A\,\mathrm{vec}(X)$ for a matrix $A\in\mathbb R^{p\times mn}$ . Its adjoint is $\mathcal A^*$ , and $\lambda_{\max}(A^\top A)=\|\mathcal A\|_2^2$ , the square of its spectral norm. Fix $b\in\mathbb R^p$ and $\mu>0$ .

Problem (1.8) is

\min_{X\in\mathbb R^{m\times n}}\ \mu\|X\|_*+\tfrac12\|\mathcal A(X)-b\|_2^2 ,

and $\mathcal X^*$ denotes its set of optimal solutions. Write $g(X)=\mathcal A^*(\mathcal A(X)-b)$ for the gradient of the data-fit term and $h(X)=X-\tau g(X)$ for a gradient step of size $\tau>0$ .

For $\nu>0$ , the matrix shrinkage operator $S_\nu$ takes a singular value decomposition $Y=U\,\mathrm{Diag}(\sigma)V^\top$ to $S_\nu(Y)=U\,\mathrm{Diag}(\bar\sigma)V^\top$ , where $\bar\sigma_i=\max(\sigma_i-\nu,0)$ . The fixed point iterations (2.1) start from an arbitrary $X^0$ and repeat

Y^k=X^k-\tau g(X^k),\qquad X^{k+1}=S_{\tau\mu}(Y^k).

Formalization targets

Goal: Theorem 4

For $\tau\in(0,2/\lambda_{\max}(A^\top A))$ and every starting point, there is $X^*\in\mathcal X^*$ with

\lim_{k\to\infty}\|X^k-X^*\|_F=0 .

The goal fixes no rate and no particular limit: it asserts convergence of the whole sequence to some minimizer.

Milestones, in attack order

Theorem 3. $S_\nu(Y)$ is an optimal solution of $\min_X\nu\|X\|_*+\tfrac12\|X-Y\|_F^2$ . This is already posed on the platform as Cai, Candès and Shen's Theorem 2.1 (which adds uniqueness) and is referenced, not restated.
Corollary 1. For every $\tau>0$ : $X^*\in\mathcal X^*$ if and only if $X^*=S_{\tau\mu}(h(X^*))$ .
Lemma 1. $\|S_\nu(Y_1)-S_\nu(Y_2)\|_F\le\|Y_1-Y_2\|_F$ , with equality if and only if $Y_1-Y_2=S_\nu(Y_1)-S_\nu(Y_2)$ .
Lemma 2. For $\tau$ in the step range, $\|h(X)-h(X')\|_F\le\|X-X'\|_F$ , and $h(X)-h(X')=X-X'$ if and only if equality holds.
Lemma 3. If $X^*\in\mathcal X^*$ , then $X\in\mathcal X^*$ if and only if $\|S_{\tau\mu}(h(X))-X^*\|_F=\|X-X^*\|_F$ .

The mission also contains the paper's Theorem 2, the optimality condition for (1.8) written with a reduced singular value decomposition $X=U\,\mathrm{Diag}(\sigma)V^\top$ : $X\in\mathcal X^*$ if and only if some $W$ satisfies $\mu(UV^\top+W)+g(X)=0$ , $U^\top W=0$ , $WV=0$ and $\|W\|_2\le1$ . The chain to Theorem 4 does not use it.

Significance

Theorem 4 is the correctness guarantee for FPC and FPCA, which were among the first algorithms to solve nuclear norm regularized problems with matrices in the thousands of rows. It certifies that the output of the plain iteration is an exact minimizer in the limit, for every starting point and every step below $2/\lambda_{\max}(A^\top A)$ . Lemmas 1–3 are the reusable part: non-expansiveness of the matrix shrinkage with a precise equality case, and the fixed point characterization of the optimal set, are the ingredients of every proximal gradient analysis with nuclear norm regularization.

Status: the theorem is proved on paper, and it is also a special case of the general convergence of forward–backward splitting. No machine-checked proof of it is known. The platform holds general forward–backward and inertial forward–backward convergence statements in Hilbert space (for example NesterovFB.Weak.theorem_3, InertialFB.IFB.theorem1_convergence) and the nonexpansiveness of abstract proximal maps (MoreauProx.Characterization.prox_nonexpansive). None is stated for the nuclear norm, for matrix shrinkage defined through the SVD, or with Ma, Goldfarb and Chen's equality cases. Formalizing this mission connects Mathlib's singular values to these operator-theoretic statements.

Difficulty

The obvious route goes through Fejér monotonicity: every step brings the iterate no farther from any minimizer, so the iterates are bounded and have a limit point. Two steps of this route do not come for free. First, the argument presupposes a minimizer; nothing in the hypotheses provides one, so the existence of an optimal solution of (1.8) has to be established from the data. Second, a limit point must be shown to be optimal, which requires the equality cases of Lemmas 1 and 2, not just the inequalities. Lemma 1's equality case concerns the singular value decompositions of two unrelated matrices whose singular vectors need not be aligned; non-expansiveness alone does not deliver it. Nonexpansive maps in general need not have convergent iterates (a rotation is nonexpansive), so continuity plus boundedness is not enough.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ. The Frobenius norm, the nuclear norm (the sum of Mathlib's LinearMap.singularValues), the linear map $\mathcal A$ as $p$ matrices Aop, its adjoint and spectral norm, and the shrinkage relation IsShrink are reused from the published Cai–Candès–Shen definitions.
$S_\nu$ is a relation, IsShrink ν Y X: $X$ is the shrinkage of $Y$ for some reduced SVD (orthonormal columns, positive singular values). Every statement takes the shrinkage output as a variable with an IsShrink hypothesis. The paper's Definition 4 also allows zero singular values, which shrink to zero and change nothing.
The step range $\tau\in(0,2/\lambda_{\max}(A^\top A))$ is written $0<\tau$ and $\tau\|\mathcal A\|_2^2<2$ , without division. For $\mathcal A=0$ this is the range $(0,\infty)$ , as on paper, rather than the empty range that Lean's $2/0=0$ would give.
$\mu>0$ is an explicit hypothesis, and so is $\nu>0$ in Lemma 1; in Corollary 1, $\tau>0$ is the only condition on the step, as on the page ("for any $\tau>0$ "). $\nu=\tau\mu$ is built into the statements.
The run of (2.1) is a predicate on the whole sequence with an arbitrary $X^0$ ; it is not the continuation scheme FPC and does not fix $X^0=0$ .
Convergence is in the Frobenius norm to some minimizer chosen after the run. Neither $\mathcal X^*\neq\emptyset$ nor boundedness of the iterates is a hypothesis; a statement that assumes either is a different, weaker theorem and is ruled out.
No statement assumes $m\le n$ ; the paper's "without loss of generality" belongs to its proofs.

A complete development needs the SVD of real matrices in terms of Mathlib's singular values, the subdifferential of the nuclear norm, and a Fejér-monotone convergence argument in finite dimension. The first two are reusable for any nuclear norm or spectral function result, and contributions of general lemmas about singular value shrinkage (functionality of IsShrink, its proximal characterization) are welcome.

Selected references

S. Ma, D. Goldfarb, L. Chen, Fixed point and Bregman iterative methods for matrix rank minimization, Math. Program. 128 (2011); preprint arXiv:0905.1643v2, 2009. https://arxiv.org/abs/0905.1643
J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://arxiv.org/abs/0810.3286
E. T. Hale, W. Yin, Y. Zhang, Fixed-point continuation for ℓ1-minimization: methodology and convergence, SIAM J. Optim. 19(3), 2008. https://doi.org/10.1137/070698920
P. L. Combettes, V. R. Wajs, Signal recovery by proximal forward-backward splitting, Multiscale Model. Simul. 4(4), 2005. https://doi.org/10.1137/050626090
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://arxiv.org/abs/0706.4138
E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://arxiv.org/abs/0805.4471

10 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments I: An Optimal Assortment Always Consists of the k Most Popular Variants for Some kResearch Paper

Motivation

A retailer deciding which variants of a product to carry (colors, sizes, flavors) trades the extra sales that variety brings against the inventory cost of stocking many low-volume items. van Ryzin and Mahajan (Management Science 45(11), 1999) gave the first model that couples a multinomial logit (MNL) choice model of consumer substitution with newsvendor inventory costs, and showed that the resulting assortment problem has a simple structure. Their paper is a standard starting point of the assortment-planning literature in operations management: the "popular set" structure it proves is the benchmark that later work on assortment optimization under MNL demand (with capacity constraints, dynamic substitution, or other choice models) compares against.

This mission formalizes the paper's first main result, Theorem 1, together with the facts its proof rests on.

Setting

A store offers a subset $S$ of the variants $N=\{1,\dots,n\}$ of a category. Each variant $j$ has an MNL preference $v_j>0$ , and the option of buying nothing has preference $v_0>0$ . A customer facing $S$ buys variant $j\in S$ with probability

q_j(S)=\frac{v_j}{\sum_{i\in S}v_i+v_0}.

Variants are labelled so that $v_1\ge v_2\ge\cdots\ge v_n$ , and the most-popular sets are $A_i=\{1,\dots,i\}$ .

The retailer sells at price $p$ and buys at unit cost $c$ , with $0<c<p$ , and stocks $x_j$ units of each variant before the season. The critical fractile is $z=\Phi^{-1}(1-c/p)$ , with $\Phi$ the standard normal distribution function. Two models of aggregate demand $Y_j$ are considered, both with store volume $\lambda>0$ :

Independent population model. $Y_j$ is normal with mean $\lambda q_j$ and standard deviation $\sigma(\lambda q_j)^\beta$ , where $\sigma>0$ and $0\le\beta<1$ . The optimal expected profit $\max_{x\ge0}\sum_{j\in S}E[p\min\{x_j,Y_j\}-cx_j]$ equals

\pi_I(S,v)=(p-c)\lambda\sum_{j\in S}q_j-\frac{p\sigma\lambda^\beta e^{-z^2/2}}{\sqrt{2\pi}}\sum_{j\in S}q_j^\beta .

Trend-following population model. All customers make the same choice, so $Y_j=\lambda$ with probability $q_j$ and $Y_j=0$ otherwise. The optimal expected profit is

\pi_T(S,v)=\sum_{j\in S}(pq_j-c)^+\lambda .

The assortment problem is $\max_{S\subseteq N}\pi(S,v)$ for $\pi=\pi_I$ or $\pi=\pi_T$ .

For Lemma 1, fix $S$ and let $\delta\ge0$ be the preference of a variant added to it: $f(\delta)=\sum_{j\in S}v_j+\delta+v_0$ , $g_I$ and $g_T$ are the numerators of the profit after the addition, and $h_I=g_I/f$ , $h_T=g_T/f$ .

Formalization targets

Goal: Theorem 1 (p. 1503)

For each demand model there is a most-popular set that is optimal among all $2^n$ assortments:

\exists\,i\in\{0,\dots,n\}\ \forall S\subseteq N:\ \pi_I(S,v)\le\pi_I(A_i,v),\qquad \exists\,i\in\{1,\dots,n\}\ \forall S\subseteq N:\ \pi_T(S,v)\le\pi_T(A_i,v).

The paper prints $i\in\{1,\dots,n\}$ for both models. In the independent model the empty assortment can be the unique optimum (when $\pi_I(A_1,v)<0$ , for instance at small $\lambda$ ), so $i=0$ is allowed there; the trend-following range is the printed one.

Milestones

(4)–(7): under normal demand, $x^*_j=\lambda q_j+z\sigma(\lambda q_j)^\beta$ is the optimal stocking vector and the optimal profit is $\pi_I(S,v)$ .
(8): under trend-following demand, stocking $\lambda$ exactly when $pq_j\ge c$ is optimal and the optimal profit is $\pi_T(S,v)$ .
Mangasarian (1969): a convex function divided by a positive affine function is quasiconvex.
Appendix: $g_I$ and $g_T$ are convex in $\delta$ on $[0,v_1]$ .
Lemma 1: $h_I$ and $h_T$ are quasi-convex on $[0,v_1]$ .
§3.1: $h(v_j)=\pi(S\cup\{j\},v)$ for $j\notin S$ , and $h(0)=\pi(S,v)$ .

Significance

The search over assortments is a priori a search over $2^n$ subsets. Theorem 1 cuts it to the $n+1$ nested sets $A_0\subset A_1\subset\cdots\subset A_n$ , so the optimal assortment is found by comparing $n+1$ numbers. The result is not obvious: the paper's example ( $n=8$ , $v_1=v_2=10$ , $v_8=1$ ) shows that $\{1,8\}$ can beat $\{1,2\}$ , so the best assortment of a given size need not be the most popular one, and yet the overall optimum is always a most-popular set. The structure is used in the paper's own comparative statics (how optimal variety moves with price, store volume and the no-purchase preference) and its comparison of fashion categories under majorization, which are the other two missions of this series.

The theorem is proved in the paper; nothing here is open. To our knowledge no part of it, nor the closed-form normal newsvendor optimum (7), has a machine-checked proof. Formalizing it fixes the edge cases the printed statement glosses over (the empty assortment, the $\beta=0$ boundary) and produces reusable pieces: the normal newsvendor profit formula and Mangasarian's ratio criterion for quasiconvexity.

Difficulty

The obvious argument, "add variants in order of popularity", fails because adding a variant both brings new sales and cannibalizes the shares of the others, and the inventory term $\sum q_j^\beta$ is concave in the shares, so profit is not monotone or submodular in $S$ in any simple sense. The proof instead compares a set with the sets obtained by removing its least popular member or exchanging it for a more popular outside variant, and needs the profit after adding a variant of preference $\delta$ to be quasi-convex in $\delta$ . That quasi-convexity is not visible from (7) directly; it requires rewriting the profit as a ratio $g/f$ with $f$ affine and proving $g_I$ convex, which in turn needs concavity of $(\sum_{j\in S}v_j^\beta+\delta^\beta)(\sum_{j\in S}v_j+\delta+v_0)^{1-\beta}$ . The exchange argument must also handle ties among the $v_j$ , which the printed proof passes over. Milestone 1 needs the derivative of the normal newsvendor objective and the identity $E(Z-z)^+=\varphi(z)-z(1-\Phi(z))$ , neither of which is in Mathlib in this form.

Formalization scope

Variants are Fin n, 0-based: the paper's variant $j$ is index $j-1$ , $A_i$ is the set of indices below $i$ , and the paper's $v_1$ is the first entry v ⟨0, _⟩. The no-purchase preference $v_0$ is a separate real v0, never a variant. Preferences are strictly positive and the sorting $v_1\ge\cdots\ge v_n$ is the hypothesis Antitone v.
Standing hypotheses: $0<c<p$ , $\lambda>0$ , $\sigma>0$ , $0\le\beta<1$ ; the goal also assumes $n\ge1$ (the trend-following range $1\le i\le n$ needs it).
$z$ is defined from $p$ and $c$ as the least $x$ with $\Phi(x)\ge1-c/p$ , $\Phi$ the c.d.f. of Mathlib's gaussianReal 0 1; a separate theorem states $\Phi(z)=1-c/p$ and uniqueness.
Powers are Real.rpow, so $0^0=1$ . At $\beta=0$ this keeps (7) correct ( $\sum_{j\in S}q_j^0=|S|$ ), but $h_I(0)=\pi_I(S,v)$ then fails; that one clause carries $\beta>0$ . The goal keeps $0\le\beta<1$ .
The positive part $(\cdot)^+$ is max · 0. In (11), $\lambda$ multiplies both terms; the printed (11) has it on the sum only, which would break $h_T(v_j)=\pi_T(S\cup\{j\},v)$ unless $\lambda=1$ .
"Optimal" means $\pi(S,v)\le\pi(A_i,v)$ for every $S\subseteq N$ , including $S=\emptyset$ . A formalization that maximizes only over prefix sets, assumes the optimum nonempty or the profit nonnegative, treats $z$ as a free real unrelated to $p$ and $c$ , or drops one of the two demand models, is a different and weaker statement and does not count.
In milestone 1 the order-up-to levels $x^*_j$ are assumed nonnegative, the formal content of the paper's assumption $\lambda^{1-\beta}q_j\gg\sigma q_j^\beta$ .

Needed infrastructure: the normal loss function and the first-order condition for the newsvendor under gaussianReal; quasiconvexity of convex-over-positive-affine ratios; concavity of weighted geometric means. The newsvendor and quasiconvexity pieces are reusable well beyond this mission. Proofs of any milestone, and alternative routes to Theorem 1 that avoid Lemma 1, are welcome.

Selected references

G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11):1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496
O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (reprinted SIAM Classics in Applied Mathematics 10, 1994). https://doi.org/10.1137/1.9781611971255
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, 1959.

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 5: Full-Batch LPT Is Within 4/3 − 1/(3m) of the Optimal Makespan on Parallel Batch MachinesResearch Paper

Motivation

Burn-in is the final reliability test of integrated circuits: boards loaded with chips are held in an oven at elevated temperature for a minimum specified time, so that marginal devices fail before shipment. An oven holds several boards at once, and a load may stay in the oven longer than its specification but never shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model such an oven as a batch processing machine and study the resulting scheduling problems. Burn-in is often the bottleneck of the test stage, which is why throughput (makespan) and due-date performance on several ovens in parallel are of practical interest.

This mission covers the paper's makespan result for parallel ovens. On ordinary identical parallel machines, Graham (SIAM J. Appl. Math. 17, 1969) proved that the LPT rule (list the jobs longest first and give each to the machine that frees up first) has worst-case ratio $4/3 - 1/(3m)$ on $m$ machines. The paper shows that the same factor holds for batch machines once the jobs are first grouped into full batches of the longest jobs.

Setting

There are $n$ jobs with processing times $p_j > 0$ , all available at time $0$ , and $m \ge 1$ identical batch processing machines. Each machine processes up to $B \ge 1$ jobs at the same time. A batch is a set of at most $B$ jobs processed together; once started it cannot be interrupted or joined, and its batch time is that of its longest job,

p(P) = \max_{j \in P} p_j .

A schedule forms the jobs into disjoint nonempty batches covering all jobs, assigns each batch to a machine, and runs every machine's batches back to back from time $0$ . The makespan is the largest machine load, the total batch time on a machine. The problem of minimizing it is written $P/B/C_{\max}$ , and $C^*$ denotes its optimal value, over every way of forming batches (any sizes up to $B$ , any grouping) and every assignment. For $B = 1$ it is the classical problem $P//C_{\max}$ .

Algorithm BLPT.

Rank the jobs in nonincreasing order of processing time and cut the ranked list into successive groups of $B$ jobs, the last possibly smaller.
Order these batches in nonincreasing order of batch time and assign each in turn to a machine with least current load.

$C(\mathrm{BLPT})$ is the resulting makespan.

For the optional lateness result, each job also has a due date $d_j \ge 0$ . The maximum lateness of a schedule is $L_{\max} = \max_j (C_j - d_j)$ , $L$ is its value under BLPT, $L^*$ its optimum and $d_{\max} = \max_j d_j$ .

Formalization targets

Goal: Proposition 3 (p. 773)

C(\mathrm{BLPT}) \le \left(\frac43 - \frac1{3m}\right) C^* .

It is claimed for every run of BLPT, whatever order the algorithm gives to equal processing times and equal batch times.

Milestones

Proposition 2 (p. 772). With the jobs re-indexed longest first, some optimal schedule has batches of consecutive jobs, all full except possibly the one containing the last job. In other words, its batches are exactly the groups formed in Step 1 of BLPT.
The reduction (§5, p. 772). $C^*$ equals the optimal makespan of $P//C_{\max}$ on the aggregate jobs $p(B_1), \dots, p(B_{\lceil n/B\rceil})$ .
Graham's LPT bound, as quoted (p. 772). For jobs $q_0 \ge \dots \ge q_{M-1} \ge 0$ on $m$ machines, list scheduling in that order has makespan at most $(4/3 - 1/(3m))$ times the optimum.
Proposition 5 (p. 773, further result).

\frac{L - L^*}{L^* + d_{\max}} \le \left(\frac13 - \frac1{3m}\right) + \frac{d_{\max}}{L^* + d_{\max}} .

Significance

Proposition 3 gives a constant-factor guarantee for a strongly NP-hard problem. The guarantee does not depend on $B$ , whereas arbitrary batch list scheduling only gets $B + 1 - 1/m$ (Proposition 1 of the same paper). For one machine the factor is $1$ , so BLPT is then exact. Proposition 2 is a structural statement: it fixes the batch composition of an optimal schedule before any assignment decision. It turns the batch problem into an ordinary parallel-machine problem, so other results for $P//C_{\max}$ transfer as well. Proposition 5 carries the guarantee over to maximum lateness, measured relative to $L^* + d_{\max}$ because $L^*$ may be negative.

All results are proved in the paper, Proposition 3 by a one-line appeal to Proposition 2 and Graham. This mission produces machine-checked versions of the reduction and the bound. Graham's LPT bound itself is not formalized anywhere on the platform. Its proof here is a reusable result about the published list-scheduling definitions, independent of batching.

Difficulty

The obvious argument is "batch as in Step 1, then apply Graham". It has two gaps. First, $C^*$ ranges over all batchings, and an optimal schedule need not use full batches or consecutive jobs. The exchange argument behind Proposition 2 has to move jobs between batches, possibly on different machines, without increasing any machine's load. Ties among equal processing times also have to be handled, since the claim is made for every longest-first ranking. Second, Graham's bound is not on the platform and has to be proved. It is a finite combinatorial statement, but its known proofs are not short. Proposition 5 additionally needs the bound for sub-instances formed by a prefix of the batches.

Formalization scope

Jobs are Fin n, 0-based. Processing times are real, p : Fin n → ℝ with 0 < p j; due dates (Proposition 5 only) are d : Fin n → ℝ with 0 ≤ d j. A batching is a list of nonempty, pairwise disjoint Finsets of size at most B covering every job. The batch time is the maximum of p over the batch.

Machine loads, assignments, the per-batching optimum and list scheduling reuse the published definitions NumStochOpt.ListScheduling.ListSchedule (firstAvailable, lsLoads, listMakespan) and NumStochOpt.ListScheduling.Makespan (machineLoad, makespan, optMakespan) from the Rinnooy Kan–Stougie mission, applied to the sequence of batch times (padded with zeros beyond the last batch, which these definitions never read). $C^*$ is the infimum of optMakespan over all valid batchings, never only over the consecutive ones of Step 1, which would assume Proposition 2.

Explicit readings of the paper's phrases:

"rank jobs in decreasing order" is any list of all jobs that is nonincreasing in p;
the batches of Step 1 are List.toChunks B of that list;
"order the batches in nonincreasing order of $p(B_k)$ " is any permutation of those chunks that is nonincreasing in batch time;
every statement is quantified over both choices;
"assign them to the machines as they become free" is least-loaded list scheduling with the published lowest-index tie rule. With no idle time, the machine that becomes free first is a least-loaded one, and the tie rule does not change the multiset of loads;
" $1/3m$ " is $1/(3m)$ ;
"optimal solution" in Proposition 2 is a valid batching with an assignment whose makespan equals $C^*$ , and "consecutive, all full except the one containing the highest indexed job" is "equal, up to order, to the chunks of the ranked list";
schedules on each machine run in list order without idle time, and every processing order is a reordering of the list. For $L^*$ this covers every semi-active schedule.

Proposition 5 adds the hypothesis $d_j \ge 0$ , which the paper's proof uses but does not print. It also makes $L^* + d_{\max}$ positive, so the printed ratios are well defined. Running times and the paper's other algorithms are out of scope.

A statement with $C^*$ restricted to consecutive batches, a sorry-free bound obtained from a degenerate $m = 0$ or empty-job reading, or a BLPT fixed to one convenient tie-break would trivialize or weaken the goal and is ruled out by the statements as posed. Welcome contributions: Graham's LPT bound on the published list-scheduling definitions (reusable for any $P//C_{\max}$ work), the exchange lemma behind Proposition 2, and the permutation invariance of optMakespan under reordering of items.

Selected references

C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. https://doi.org/10.1137/0117039
A. H. G. Rinnooy Kan, L. Stougie, Stochastic Integer Programming, Ch. 8 of Y. Ermoliev, R. J.-B. Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer, 1988 (source of the reused list-scheduling definitions). https://doi.org/10.1007/978-3-642-61370-8

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 3: Dynamic Program DP3 Minimizes the Number of Tardy Equal-Length Jobs on a Batch Machine with Agreeable Release and Due DatesResearch Paper

Motivation

Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).

Setting

There are $n$ jobs and one batch processing machine with capacity $B\ge1$ . Job $j$ has release time $r_j$ , due date $d_j$ , and processing time $p_j$ . In the main problem every processing time equals a common value $p$ . A batch is a nonempty set of at most $B$ jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.

The completion time $C_j(S)$ of job $j$ in schedule $S$ is the completion time of its batch. A job is on time when $C_j(S)\le d_j$ and tardy when $d_j<C_j(S)$ . Write $U(S)=\#\{j:d_j<C_j(S)\}$ and let $U^*$ be the minimum of $U(S)$ over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.

For the structural lemmas, agreeable release times and due dates mean that $r_i<r_j$ implies $d_i\le d_j$ . For the dynamic program, jobs are indexed so that both $r_j$ and $d_j$ are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).

Formalization targets

Structural optimal schedules

Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which $U^*$ is defined.

Correctness of Algorithm DP3

Let $f(i,j)$ be the table defined by Algorithm DP3 for the first $j$ jobs and a selected count $i$ of on-time jobs. Its boundary values are $f(0,j)=0$ and $f(i,j)=+\infty$ for $i>j$ . For $1\le i\le j$ , it takes the minimum of $f(i,j-1)$ and the eligible transitions that append a batch of $k$ jobs, $1\le k\le\min(B,i)$ . A transition uses $\max\{f(i-k,j-k),r_j\}+p$ and is eligible when that completion time does not exceed $d_{j-k+1}$ . The main target is

U^*=n-\max\{i\in\{0,\ldots,n\}:f(i,n)<+\infty\}.

The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).

Unequal processing times

The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common $p$ by $f(i-k,j-k)+p_j$ . The corresponding correctness statement is a further milestone (p. 771).

Significance

The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.

The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.

Difficulty

The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.

Formalization scope

Jobs use Fin n, with index zero representing the paper's job 1; the table's $j$ is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; $+\infty$ in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most $B$ , pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.

The strict implication $r_i<r_j\Rightarrow d_i\le d_j$ makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that $r_j$ is the last batch's latest release and $d_{j-k+1}$ its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range $1\le k\le\min(B,i)$ , with an empty range giving $+\infty$ . Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.

This mission covers correctness only. The paper's $O(n^2B)$ running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.

Selected references

C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 1992, pp. 764–775. DOI: 10.1287/opre.40.4.764.

9 thms2 active usersReviewed

Numerical Analysis·Captain: mikedeng1

Convergence Analysis of Some Algorithms for Solving Nonsmooth Equations I: At a Semismooth, Strongly BD-Regular Zero the ∂_B Newton Method Converges Superlinearly and ‖F‖ Decreases SuperlinearlyResearch Paper

Motivation

Many problems of operations research reduce to a system of nonsmooth equations $F(x)=0$ with $F:\mathbb R^n\to\mathbb R^n$ locally Lipschitz but not differentiable: the nonlinear complementarity problem $h(x)\ge 0$ , $f(x)\ge0$ , $h(x)^Tf(x)=0$ becomes $F(x)=\min\{h(x),f(x)\}=0$ componentwise, and variational inequalities, KKT systems and max-type equations admit similar reformulations. Newton's method is the natural local solver, but it needs a substitute for the Jacobian at points where $F$ is not differentiable.

Timeline:

1977. Mifflin introduces semismooth functionals.
1987–1990. Robinson proposes B-derivatives; Pang (1990) and Harker–Xiao (1990) study Newton methods based on directional derivatives (Math. Oper. Res. 15; Math. Programming 48).
1993. Qi and Sun (Math. Programming 58) prove local superlinear convergence of $x^{k+1}=x^k-V_k^{-1}F(x^k)$ , $V_k\in\partial F(x^k)$ , assuming every element of Clarke's generalized Jacobian $\partial F(x^*)$ is nonsingular.
1993. Qi (Math. Oper. Res. 18), the source of this mission, observes that this assumption already fails for $f(x)=|x|$ , where $\partial f(0)=[-1,1]$ contains $0$ , and restricts $V_k$ to the smaller B-subdifferential. Nonsingularity is then needed only on $\partial_B F(x^*)$ .

Setting

A map $F:\mathbb R^n\to\mathbb R^m$ is locally Lipschitz throughout; the norm is the Euclidean 2-norm. Let $D_F$ be the set of points where $F$ is differentiable (almost every point, by Rademacher's theorem). The B-subdifferential of $F$ at $x$ is

\partial_B F(x)=\Big\{\lim_{i\to\infty}\nabla F(x_i)\;:\;x_i\to x,\ x_i\in D_F\Big\},

and Clarke's generalized Jacobian is its convex hull, $\partial F(x)=\operatorname{conv}\partial_B F(x)$ . The directional derivative is $F'(x;h)=\lim_{t\downarrow0}(F(x+th)-F(x))/t$ . $F$ is semismooth at $x$ if $\lim Vh'$ over $V\in\partial F(x+th')$ , $h'\to h$ , $t\downarrow 0$ , exists for every $h$ . A map $F:\mathbb R^n\to\mathbb R^n$ is strongly BD-regular at $x$ if every $V\in\partial_B F(x)$ is nonsingular.

The $\partial_B$ Newton method is

x^{k+1}=x^k-V_k^{-1}F(x^k),\qquad V_k\in\partial_B F(x^k), \tag{3.2}

with any choice of $V_k$ , and the directional-derivative Newton method is $x^{k+1}=x^k+d^k$ with $F(x^k)+F'(x^k;d^k)=0$ (3.11)–(3.12). In Lean, $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\partial_B F$ is NonsmoothNewton.Shared.bJac F, $\partial F$ is clarkeJac F, semismoothness is NonsmoothNewton.Local.SemismoothAt, and a run of (3.2) is IsBDNewtonRun F x V.

Formalization targets

Goal: Theorem 3.1 (p. 234)

If $F(x^*)=0$ and $F$ is semismooth and strongly BD-regular at $x^*$ , there is $\delta>0$ such that every $V\in\partial_B F(y)$ , $\|y-x^*\|<\delta$ , is nonsingular with $\|y-V^{-1}F(y)-x^*\|<\delta$ , and every run of (3.2) from $\|x^0-x^*\|<\delta$ satisfies

x^k\to x^*,\qquad \|x^{k+1}-x^*\|=o(\|x^k-x^*\|),

and, when $F(x^k)\ne0$ for all $k$ ,

\lim_{k\to\infty}\frac{\|F(x^{k+1})\|}{\|F(x^k)\|}=0. \tag{1.9}

Milestones

Lemma 2.6 (p. 233): near a strongly BD-regular point, every $V\in\partial_B F(y)$ is nonsingular with $\|V^{-1}\|\le c$ , and $\|h\|\le c\|F'(y;h)\|$ where $F$ is semismooth.
Lemma 2.2 (1) ⇔ (3) (p. 230): semismoothness at $x$ is equivalent to $Vh-F'(x;h)=o(\|h\|)$ for $V\in\partial F(x+h)$ . This is the published item NonsmoothNewton.Local.theorem_2_3.
(2.2) (p. 229) at a semismooth point: $F(x+h)=F(x)+F'(x;h)+o(\|h\|)$ . This is the published item NonsmoothNewton.Local.remark_2_17.
Corollary 3.2 (p. 235): for every $\varepsilon>0$ , one $\partial_B$ Newton step near $x^*$ contracts $\|x-x^*\|$ and $\|F(x)\|$ by the factor $\varepsilon$ .

Further statements of the paper in this mission

Lemma 2.3 (degree-2 semicontinuity, p. 230); the quadratic second paragraph of Theorem 3.1; Corollary 3.3 (the directional-derivative method, p. 235); Lemma 2.2 (1) ⇔ (2); and the counterexample of Final Remark (6) (pp. 243–244), which shows that (3.12) need not be solvable near a semismooth, strongly BD-regular zero.

Significance

Theorem 3.1 is the local convergence theorem for the semismooth Newton method in the form most used later: the B-subdifferential version under strong BD-regularity is what generalized Newton methods for complementarity problems (through the min and Fischer–Burmeister reformulations) rely on, because $\partial_B F$ is finite in typical piecewise-smooth examples while $\partial F$ is a polytope that may contain singular matrices. The statement (1.9) makes the method a descent method for $\|F\|$ near the solution, which is how the paper later globalizes it (damped Newton, §4; hybrid method, §6). Corollary 3.2 is reused verbatim in the analysis of the damped method.

The results are proved in the paper; none of them is formalized. The mission produces a machine-checked version of the local theory, on top of the published B-subdifferential and semismoothness definitions of the Qi–Sun series, and makes the Clarke-to-B-subdifferential refinement available to later missions.

Difficulty

The Clarke-Jacobian argument cannot be copied. There, nonsingularity of the compact convex set $\partial F(x^*)$ propagates to a neighbourhood by upper semicontinuity of $\partial F$ . Here only the extreme set $\partial_B F(x^*)$ is assumed nonsingular, and its convex hull may contain singular matrices. Lemma 2.6 therefore has to work with limits of genuine Jacobians, and the error estimate (3.3) has to combine an estimate stated for $\partial F(x^k)$ , namely Lemma 2.2, with the bound on $V_k^{-1}$ , which exists only for $V_k\in\partial_B F(x^k)$ . A second subtlety is (1.9), which needs a lower bound $\|x^k-x^*\|\le\frac{c}{1-\varepsilon}\|F(x^k)\|$ that does not follow from superlinear convergence alone.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with the 2-norm and the spectral operator norm, as the paper fixes ("we use 2-norms"). The dimension $n=0$ is allowed.
Standing assumption. Every statement carries LocallyLipschitz F (§1, p. 227).
Nonsingularity is the existence of a two-sided inverse $W$ (IsInverse V W), never a junk inverse. A run of (3.2) is written $V_k(x^{k+1}-x^k)=-F(x^k)$ without an inverse, so nonsingularity of $V_k$ is a conclusion.
Quantifier order. $\delta$ is chosen before the run and serves every starting point within $\delta$ and every choice $V_k\in\partial_B F(x^k)$ . Writing "for every run there is a $\delta$ " would trivialize the theorem and is ruled out.
(1.9) is stated under the paper's hypothesis $F(x^k)\ne0$ for all $k$ , since otherwise the quotient is not defined.
Disclosed deviations.
- Corollary 3.2 is stated for $\varepsilon>0$ (the page prints $\varepsilon\ge0$ , false at $0$ ).
- Corollary 3.3 adds semismoothness of $F$ on a neighbourhood of $x^*$ , which its printed proof uses through Lemma 2.6's (2.16).
- $O(\cdot)$ and "quadratic" are pinned to explicit constants.
Infrastructure needed.
- Rademacher-type facts for $\partial_B F$ : nonemptiness, compactness and closed graph. The platform already has WillR's proved lemmas NonsmoothNewton.Shared.exists_local_bJac_control, bJac_mem_of_tendsto, isCompact_bJac.
- Perturbation bounds for inverses.
- The relation between directional derivatives and $\partial_B F$ at semismooth points.
These are reusable for the other two missions of this series and for later semismooth Newton developments. Proofs of the milestones, and alternative arguments, are welcome.

Selected references

L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Math. Oper. Res. 18(1):227–244, 1993. https://doi.org/10.1287/moor.18.1.227
L. Qi and J. Sun, A nonsmooth version of Newton's method, Math. Programming 58:353–367, 1993. https://doi.org/10.1007/BF01581275
J.-S. Pang, Newton's method for B-differentiable equations, Math. Oper. Res. 15(2):311–341, 1990. https://doi.org/10.1287/moor.15.2.311
R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15(6):959–972, 1977. https://doi.org/10.1137/0315061
A. Shapiro, On concepts of directional differentiability, J. Optim. Theory Appl. 66:477–487, 1990. https://doi.org/10.1007/BF00940933

9 thms2 active usersReviewed

Convex Optimization Operations Research·Captain: mikedeng1

Primal-Dual Interior-Point Methods for Self-Scaled Cones I: After One Short Step from N(β), λ₂(x₊, s₊) ≤ (2 + δ − κ)(ϵ + κ)²/((1 − δ)²(1 − κ)³)Research Paper

Motivation

Linear programming, second-order cone programming and semidefinite programming are all instances of conic linear programming: minimize a linear function over the intersection of an affine subspace with a closed convex cone. Primal-dual interior-point methods solve these problems in polynomially many iterations and are the algorithms behind most conic solvers in practical use. Nesterov and Todd showed that the primal-dual path-following analysis known for linear programming extends verbatim to every cone that admits a self-scaled barrier, a class containing the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products (Nesterov & Todd 1997; Nesterov & Todd 1998).

Timeline. Kojima, Mizuno and Yoshise (1989) and Monteiro and Adler (1989) gave short-step primal-dual path-following methods for linear programming with an $O(\sqrt n \ln(1/\varepsilon))$ iteration bound. Mizuno, Todd and Ye (1993) added the predictor-corrector variant. Nesterov and Nemirovskii (1994) developed the general theory of self-concordant barriers. Nesterov and Todd (1997) introduced self-scaled barriers and scaling points; the 1998 paper analysed the short-step, adaptive-step and predictor-corrector methods for them. Güler (1996) identified self-scaled cones with symmetric (homogeneous self-dual) cones.

Setting

Let $E = \mathbb R^n$ with inner product $\langle\cdot,\cdot\rangle$ , and let $K \subseteq E$ be a closed convex cone that is pointed and has nonempty interior; $K^* = \{s : \langle s, x\rangle \ge 0\ \forall x \in K\}$ is its dual cone. A linear map $A : \mathbb R^n \to \mathbb R^m$ (surjective), $b \in \mathbb R^m$ and $c \in \mathbb R^n$ define the primal problem $\min\{\langle c, x\rangle : Ax = b,\ x \in K\}$ and its dual $\max\{\langle b, y\rangle : A^*y + s = c,\ s \in K^*\}$ . Strictly feasible points are $x \in S^0(P)$ ( $x \in \operatorname{int} K$ , $Ax = b$ ) and $(y, s) \in S^0(D)$ ( $s \in \operatorname{int}K^*$ , $A^*y + s = c$ ).

A $\nu$ -self-concordant logarithmically homogeneous barrier $F$ for $K$ is a self-concordant convex function on $\operatorname{int} K$ that tends to $+\infty$ at the boundary, satisfies $(\langle F'(x), h\rangle)^2 \le \nu\langle F''(x)h, h\rangle$ and $F(\tau x) = F(x) - \nu\ln\tau$ . Its conjugate is $F_*(s) = \sup_{x \in \operatorname{int}K}\{-\langle s, x\rangle - F(x)\}$ . The barrier is self-scaled if $F''(w)x \in \operatorname{int}K^*$ and $F_*(F''(w)x) = F(x) - 2F(w) - \nu$ for all $w, x \in \operatorname{int}K$ . For $x \in \operatorname{int}K$ and $s \in \operatorname{int}K^*$ the scaling point is the $w \in \operatorname{int}K$ with $F''(w)x = s$ .

Local norms at $x \in \operatorname{int}K$ are $\|v\|_x = \langle F''(x)v, v\rangle^{1/2}$ for primal vectors and $\|u\|_x = \langle [F''(x)]^{-1}u, u\rangle^{1/2}$ for dual vectors; $|u|_x$ is the cone-induced (max-type) norm. With $\mu(x, s) = \langle s, x\rangle/\nu$ the proximity measures are

\lambda_2(x, s) = \Big\|\frac{s}{\mu(x,s)} + F'(x)\Big\|_x,\qquad \lambda_\infty(x, s) = \Big|\frac{s}{\mu(x,s)} + F'(x)\Big|_x,

and $\bar\lambda_2(x, s, \mu) = \|s/\mu + F'(x)\|_x$ . The narrow neighbourhood is $N(\beta) = \{(x,y,s) \in S^0(P)\times S^0(D) : \lambda_2(x, s) \le \beta\}$ .

The short step from $(x, y, s) \in N(\beta)$ targets $\mu_+ = (1 - \kappa/\sqrt\nu)\mu(x,s)$ and solves

F''(w)q_x + q_s = s + \mu_+F'(x),\qquad Aq_x = 0,\qquad A^*q_y + q_s = 0,

then sets $(x_+, y_+, s_+) = (x - q_x, y - q_y, s - q_s)$ .

Formalization targets

Goal: Theorem 6.4

With $\delta = \lambda_\infty(x,s)$ , $\epsilon = \lambda_2(x,s)$ , $\epsilon_+ = \bar\lambda_2(x, s, \mu_+)$ and $\eta = \epsilon_+/(1-\delta) < 1$ :

x_+ \in \operatorname{int}K,\quad s_+ \in \operatorname{int}K^*,\quad \mu(x_+, s_+) = \mu_+,\quad \lambda_2(x_+, s_+) = \bar\lambda_2(x_+, s_+, \mu_+) \le \frac{(2 + \delta - \kappa)(\epsilon + \kappa)^2}{(1-\delta)^2(1-\kappa)^3}.

The constant $\kappa \in (0,1)$ and $\beta \in (0,1)$ are free; no numerical choice is hard-coded.

Milestones

Theorem 3.6 (norms at neighbouring points), Lemma 3.13 and Corollary 3.14 (scaling-point Hessian versus the Hessians at $x$ and $s$ ), Lemma 6.2 (effect of decreasing $\mu$ ), (6.10) (the gap after the step), and Lemma 6.3 (size of the step, feasibility, norms at $x_+$ ).

Companion results

The Algorithm 6.1 invariant ( $\beta = 1/10$ , $\kappa = 1/15$ : iterates stay in $N(1/10)$ while $\mu$ shrinks by $1 - (15\sqrt\nu)^{-1}$ ), Theorem 6.5 (the predictor step length $\alpha^* \ge (10\sqrt\nu)^{-1}$ ), and Lemma 6.1.

Significance

Theorem 6.4 is the one-step estimate behind the $O(\sqrt\nu\ln(\langle s_0, x_0\rangle/\zeta))$ iteration bound of the short-step method on every symmetric cone, and with it of the most widely used complexity bounds for semidefinite and second-order cone programming. The same estimate, with $\kappa = 0$ , certifies the corrector step of the predictor-corrector method (Algorithm 6.3).

The results are proved in the paper; none is formalized. A Lean development would provide a machine-checked core of conic interior-point theory: the local-norm calculus of self-scaled barriers (Theorem 3.6, Lemma 3.13), which is reused across all the methods of the paper, and a verified complexity statement for an algorithm family used in practice. The companion mission on the functional-proximity method (Theorem 7.1 of the same paper) shares the setting.

Difficulty

The obvious argument expands $s_+ + \mu_+F'(x_+)$ and bounds each term by self-concordance. Generic self-concordance controls norms at a new point only under $\|x_+ - x\|_x < 1$ and gives constants that do not close the recursion with $\beta = 1/10$ ; it also says nothing about the dual side. The proof needs properties special to self-scaled barriers: the scaling point $w$ and the two-sided comparison of $F''(w)/\mu$ with $F''(x)$ (Lemma 3.13), norm comparisons under the weaker hypothesis $|x_+ - x|_x < 1$ (Theorem 3.6), and a third-derivative bound from Nesterov–Todd 1997. In Lean, none of the self-scaled barrier theory, conjugate barriers on cones, or local norms exists in Mathlib.

Formalization scope

$E$ is EuclideanSpace ℝ (Fin n) and $E^*$ is identified with $E$ through the inner product. Because the paper distinguishes primal and dual norms by the space of the argument, the formalization names them: lnorm G v u (same space as $v$ ) and dnorm G v u (other space, through the inverse Hessian), for $G = F$ or $G = F_*$ ; sigma C c u and absn C c u take the cone and the centre explicitly. The conjugate is a real supremum over $\operatorname{int}K$ and is only evaluated in $\operatorname{int}K^*$ . $\lambda_2$ , $\lambda_\infty$ use the first of their two printed forms.

Standing assumptions carried by every statement: $K$ proper, $F$ a $\nu$ -self-scaled barrier, and $\nu \ge 1$ (a consequence of pointedness that the paper derives). The barrier definition adds positive definiteness of $F''$ on $\operatorname{int}K$ , implied by the other conditions for a pointed cone. Theorem 6.4 adds $0 < \kappa < 1$ (the paper's "some fixed constant", forced by its proof) and the conclusion $x_+ \in \operatorname{int}K$ , $s_+ \in \operatorname{int}K^*$ from Lemma 6.3. Assumptions (2.4)–(2.5) are implied by the strictly feasible starting point. In Theorem 3.6 the middle factors of (3.12) are corrected to $(1 - p_+)$ and $(1 + p_-)$ ; the printed ones fail for the half-line.

Search directions are any solution of their linear systems; their existence is not assumed. The goal assumes no bound from Lemmas 6.2–6.3 and no value of $\mu(x_+, s_+)$ , so it cannot be discharged by restating its hypotheses.

Needed infrastructure: derivatives of logarithmically homogeneous functions ((2.7)–(2.10)), properties of the conjugate barrier ((2.12)–(2.16)), the existence and properties of scaling points (Nesterov–Todd 1997), and the local norm inequalities of self-concordant functions. These are reusable for any interior-point formalization; contributions of such lemmas are welcome.

Selected references

Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Math. Oper. Res. 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
O. Güler, Barrier functions in interior point methods, Math. Oper. Res. 21 (1996) 860–885. https://doi.org/10.1287/moor.21.4.860
M. Kojima, S. Mizuno and A. Yoshise, A primal-dual interior point algorithm for linear programming, in Progress in Mathematical Programming, Springer, 1989, 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
S. Mizuno, M. J. Todd and Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Math. Oper. Res. 18 (1993) 964–981. https://doi.org/10.1287/moor.18.4.964

11 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 2: Branch and Bound with the Two-Machine Lower Bound Finds a Sequence of Least Mean Completion TimeResearch Paper

Motivation

In a two-machine flow shop, each of $n$ jobs is processed first on machine $A$ and then on machine $B$ , and the order of the jobs is to be chosen. For the makespan (the finishing time of the last job), Johnson (1954) gave an exact sorting rule. For the sum (equivalently, the mean) of the completion times, no such rule is known: the problem is NP-hard in the strong sense (Garey, Johnson and Sethi, 1976), and exact methods search the $n!$ sequences implicitly.

Ignall and Schrage (1965) were among the first to apply branch and bound to sequencing. They view the $n!$ sequences as the leaves of a tree of partial sequences, keep a list of partial sequences ranked by a lower bound, and always extend the most promising one. For the two-machine mean-completion-time problem they introduced a lower bound, built from two relaxations (one where machine $A$ is the bottleneck, one where machine $B$ is), that became the template for many later flow-shop bounds.

Setting

There are $n\ge1$ jobs; job $i$ has processing time $a_i$ on machine $A$ and $b_i$ on machine $B$ . A sequence is a permutation $\sigma$ of the jobs, processed in that order on both machines with every operation started as early as possible. The completion time $d_i(\sigma)$ of job $i$ is the time machine $B$ finishes it, and the objective is $\sum_{i=1}^n d_i(\sigma)$ .

A node $J_r$ is a partial sequence of $r$ jobs; $\bar J_r$ is the set of the $n-r$ jobs not in it; $k$ is the last job of $J_r$ and $d_k$ its completion time; $d_i$ ( $i\in J_r$ ) are the completion times of the jobs of $J_r$ . For an ordering $(i_1,\dots,i_{n-r})$ of $\bar J_r$ ,

T_r=\sum_{p=1}^{n-r}\Big[\sum_{j\in J_r}a_j+(n-r-p+1)a_{i_p}+b_{i_p}\Big],

and for an ordering $(j_1,\dots,j_{n-r})$ of $\bar J_r$ ,

S_r=\sum_{p=1}^{n-r}\Big[\max\Big(d_k,\sum_{j\in J_r}a_j+\min_{i\in\bar J_r}a_i\Big)+(n-r-p+1)b_{j_p}\Big].

$\hat T_r$ and $\hat S_r$ are their minima over all orderings of $\bar J_r$ , and the lower bound of the node is

LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r).

The procedure starts with a list holding only the empty node. A step removes the first node, creates one child for every unscheduled job by appending it, and inserts the children into the list ranked by $LB$ (a new node goes before old nodes with equal bound). It stops the first time the first node of the list is terminal, i.e. has scheduled $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the procedure finds a sequence of least mean completion time

For all real data, (i) the procedure reaches a list whose first node $P$ is terminal, and (ii) whenever that happens, the sequence $\sigma^\ast$ formed by $P$ and its one unscheduled job satisfies

\sum_{i=1}^n d_i(\sigma^\ast)\le\sum_{i=1}^n d_i(\sigma)\qquad\text{for every sequence }\sigma .

Milestones

For $1\le r\le n-1$ and every sequence $\sigma$ beginning with $J_r$ : $T_r$ of the order in which $\sigma$ processes $\bar J_r$ is at most $\sum_{i\in\bar J_r}d_i(\sigma)$ , hence so is $\hat T_r$ (pp. 405–406).
An ordering of $\bar J_r$ by increasing $a_i$ attains $\hat T_r$ (p. 406).
An ordering of $\bar J_r$ by increasing $b_j$ attains $\hat S_r$ (p. 406).
The analogue of 1 for $S_r$ and $\hat S_r$ (p. 406).
$LB(J_r)\le\sum_i d_i(\sigma)$ for every $\sigma$ beginning with $J_r$ (p. 406).
At depth $n-1$ , $LB$ equals the value of the node's unique completion (labelled: what the stopping rule of p. 402 needs).
Without delays, job $i_p$ completes at $\sum_{J_r}a_j+a_{i_1}+\dots+a_{i_p}+b_{i_p}$ and $\sum_{\bar J_r}d_i=T_r$ (pp. 405–406).
The three-job example of p. 408: 1–2 is optimal for jobs 1, 2, while 3–2–1 is optimal for all three.

Significance

The goal is the correctness of the paper's algorithm for the two-machine problem: the sequence it returns is optimal, not merely good, and it returns one for every input. The lower-bound milestones are the paper's own justification of its bound, and the sorting milestones show that the bound is computable in $O(n\log n)$ per node rather than by a minimization over $(n-r)!$ orderings.

On the formal side, no item on the platform treats flow-shop lower bounds or branch and bound over sequences; the nearest is the branch-and-bound mission for jointly constrained biconvex programs (BiconvexProg.BranchBound, Al-Khayyal and Falk 1983), an unrelated algorithm over boxes. The paper's arguments are short and informal ("it should be evident"); the formalization makes explicit that the $S_r$ bound holds for every order and every input, which the paper derives only by analogy with $T_r$ . The published definitions of Johnson's as-soon-as-possible schedule (from the Johnson 1954 missions) are reused for the completion times.

Difficulty

The two halves of the bound are relaxations of different kinds. $T_r$ ignores waiting on machine $B$ ; $S_r$ ignores idle time on machine $B$ after its first job of $\bar J_r$ and replaces that job's machine- $A$ time by the smallest one. The paper's description of $S_r$ as "the sum of the completion times" when $\min b\ge\max a$ is not an identity, since $\min a$ replaces $a_{j_1}$ ; only the inequality is true, and it has to be proved for the given order directly. The sorting claims are rearrangement inequalities, with the coefficient $n-r-p+1$ decreasing in the position.

The goal is a statement about all $n!$ sequences, while the procedure only ever looks at the nodes on its list, whose length changes at every step. The tempting one-line justification, that the first terminal node has the smallest bound, says nothing by itself about sequences that are not descendants of nodes still on the list, nor about whether the bound of a terminal node is the value of its sequence; and termination of the search has to be shown, not assumed.

Formalization scope

Jobs are Fin n (the paper's $1,\dots,n$ shifted to $0,\dots,n-1$ ); processing times are arbitrary reals, with no sign condition; all statements are true without one.
Completion times of a full sequence come from Johnson's asapC2 (referenced definition JohnsonFlowShop.TwoStage.asapStart2). The objective is the sum of the completion times; the paper's mean differs by the fixed factor $1/n$ .
A node is a list of jobs; "a sequence begins with $J_r$ " means $J_r$ is a prefix of its list of jobs.
$\hat T_r$ and $\hat S_r$ are defined as minima over all orderings of $\bar J_r$ , not by a sorted order; that sorting attains them is milestones 2 and 3. Defining them by sorting would make those milestones true by definition.
At the root ( $r=0$ ) $d_k$ is read as $0$ ; the root is never ranked, and the lower-bound milestones are stated for $1\le r\le n-1$ .
Terminal nodes are at depth $n-1$ . The paper says "a node that has scheduled all $n$ jobs"; its own example stops at a node with three of four jobs, and its node counts end at level $n-1$ .
Explicit readings: "is a lower bound" means $\le$ the objective of every sequence beginning with the node; "will exceed" means $\ge$ ; "the problem is solved: that node's sequence is an optimal one" means termination plus optimality over all $n!$ sequences.
A trivializing formalization is ruled out: the bound is not taken over an unrestricted or empty set of orderings (the set of orderings of $\bar J_r$ is nonempty), optimality is over all permutations rather than over the nodes the run visits, and termination is part of the goal.
Not formalized: the reduction to permutation schedules (the paper's footnote on p. 401 asserts it for mean completion time without proof, and no platform item proves it), dominance discarding (pp. 403–405), the jobset generator, Tables I–III and the 9-job examples.

Proofs of any milestone, and reusable lemmas on as-soon-as-possible two-machine schedules (completion times of a prefix, monotonicity in the start time), are welcome.

Selected references

E. Ignall and 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
M. R. Garey, D. S. Johnson and R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
A. H. Land and A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Monotone Comparative Statics I: The Argmax Is Monotone Nondecreasing in (t, S) If and Only If f Is Quasisupermodular in x and Has the Single Crossing Property in (x; t)Research Paper

Why monotone comparative statics matters

An optimization problem often changes when a parameter changes: a price rises, a constraint expands, or a strategic environment shifts. Comparative statics asks whether the optimal choice moves in a predictable direction. The usual numerical tools, such as derivatives, can be unavailable when choices form a discrete set or the objective is neither smooth nor concave. Milgrom and Shannon's Monotonicity Theorem gives a condition expressed entirely through order and preference comparisons. It applies to individual optimization problems and supplies the order argument used later in their paper for games with strategic complementarities.

Their 1994 paper moves beyond cardinal conditions such as supermodularity and increasing differences. Those conditions imply useful comparative statics, but they can change under a strictly increasing transformation of the objective even though every argmax set stays the same. Quasisupermodularity and single crossing describe the comparisons that actually govern the argmax. The theorem characterizes these conditions through the behavior of optimizers over all constraint sets, rather than giving only a sufficient test. The historical relationship and the claims in this paragraph are described in Milgrom and Shannon, Sections 1–2.

Ordered choices, constraints, and preferences

Let $X$ be a lattice: a partially ordered choice set in which every two choices $x,y$ have a meet $x\wedge y$ and a join $x\vee y$ . Let $T$ be a partially ordered parameter set and $f:X\times T\to\mathbb R$ an objective. For any constraint set $S\subseteq X$ , define the possibly empty maximizer set

M(t,S)=\operatorname{argmax}_{x\in S}f(x,t)=\{x\in S: f(y,t)\le f(x,t)\text{ for every }y\in S\}.

The strong set order, written $A\le_s B$ , compares subsets of the lattice by requiring $a\wedge b\in A$ and $a\vee b\in B$ for every $a\in A$ and $b\in B$ . It can compare feasible sets as well as sets of optimizers. On singleton sets it agrees with the order on $X$ . It also holds vacuously if either set is empty; it is reflexive at $S$ exactly when $S$ is a sublattice. These are the paper's conventions on page 159.

A function $g:X\to\mathbb R$ is quasisupermodular if, for every $x,y\in X$ , both

g(x\wedge y)\le g(x)\Rightarrow g(y)\le g(x\vee y),\qquad g(x\wedge y)<g(x)\Rightarrow g(y)<g(x\vee y)

hold. The single crossing property of $f$ in $(x;t)$ requires, whenever $x''<x'$ and $t''<t'$ , that a weak or strict preference for $x'$ over $x''$ at $t''$ remains respectively weak or strict at $t'$ . The strict version sends even a weak preference at $t''$ to a strict one at $t'$ . These definitions are given on pages 160 and 162.

Formalization targets

Theorem 4: the monotonicity equivalence

The main target is Theorem 4 on page 162:

\bigl[\forall t\le t',\ S\le_s S': M(t,S)\le_s M(t',S')\bigr] \quad\Longleftrightarrow\quad \bigl[\forall t,\ f(\cdot,t)\text{ is quasisupermodular on }X\bigr] \land\bigl[f\text{ has single crossing in }(x;t)\bigr].

The milestone list records the two necessity claims and the sufficiency claim separately, using the three corresponding passages of the paper's proof. The goal keeps both directions together. It imposes no restriction on which subsets may be used as constraints.

Consequences and the stronger selection statement

Corollary 1 characterizes quasisupermodularity alone through monotonicity as the constraint set changes, with no varying parameter. Corollary 2 says that the maximizers over a sublattice themselves form a sublattice. The reflexivity remark identifies when $S\le_s S$ holds. Theorem 4′ uses the strict single crossing property and a nondecreasing feasible-set correspondence $S:T\to 2^X$ to conclude that every selection of maximizers is nondecreasing. These nearby results share the definition layer with the main theorem and give distinct targets for the formal development.

What the result supplies

The equivalence turns an order property of an entire family of optimization problems into two properties of the objective. In particular, its converse shows that if every feasible-set comparison produces monotone maximizers, then quasisupermodularity and single crossing are forced. This matters for problems where an analyst can reason about choice behavior more directly than about algebraic properties of $f$ . The corollaries also separate the effects of constraints and parameters and describe the structure of the optimal-choice set. The paper develops these consequences on pages 162–163.

The theorem is proved in the paper. The remaining work here is a machine-checked Lean proof of the ordinal characterization, its two directions, and the adjacent consequences. Published Prove2Me definitions already encode the strong set order, and its Topkis series covers related cardinal hypotheses such as supermodularity and increasing differences. This mission adds the paper's quasisupermodularity and single crossing predicates and seeks formal proofs of the distinct ordinal results. The separate characterization and linear-perturbation results of the same paper are targets of the other missions in this series.

Where the proof is difficult

The obstacle is the interaction of two orders. An increase in $t$ changes preferences, while an increase in $S$ changes which choices can be compared. A pointwise claim that an optimizer rises does not follow from either order condition alone, particularly when maximizers tie or are incomparable. The main theorem concerns sets of maximizers under the strong set order, so both the meet and join of optimizers at two parameter–constraint pairs must land in the correct maximizing sets. Conversely, observing monotonicity for one fixed feasible set cannot establish quasisupermodularity; the equivalence relies on monotonicity across every constraint set. The weak and strict preference clauses have different roles, so replacing either by the other changes the target. These are the distinctions visible in Theorem 4 and its proof.

Formalization scope

Lean represents $X$ with Lattice, $T$ with PartialOrder, and $f:X\to T\to\mathbb R$ in curried form. No finiteness, total order, topology, measurability, or maximizer-attainment hypothesis is imposed. The paper's product order for product lattices is Lean's usual componentwise order. The imported Supermodularity.Lattices.InducedSetOrder is exactly the paper's strong set order, including its behavior on empty sets. The definition argmaxOn returns the set of points in $S$ whose objective value bounds every value attained in $S$ ; it may be empty.

Quasisupermodularity is encoded with a reusable set argument but applied to Set.univ in every theorem here, so the property concerns the whole lattice. Single crossing compares strictly ordered choices and strictly ordered parameters and preserves both weak and strict preferences. ArgmaxMonotone compares weakly ordered parameters and all constraint sets under the strong set order. Theorem 4′ encodes a selection on an arbitrary domain $D\subseteq T$ where maximizers actually exist; it makes no global existence assertion. For Corollary 2, an arbitrary parameter is fixed and its objective is written $g:X\to\mathbb R$ .

These choices rule out easy specializations that would change the theorem: taking $X$ to be a chain, restricting quasisupermodularity to a selected feasible set, demanding nonempty argmax sets, or dropping strict preference clauses. The reusable development consists of the maximizer-set definition, the two ordinal predicates, and their relation to the published strong set order. Contributions proving the goal, its three proof-direction milestones, the corollaries, and the selection theorem all fit this scope.

Selected references

Paul Milgrom and Chris Shannon, Monotone Comparative Statics, Econometrica 62(1), 1994, 157–180. DOI: 10.2307/2951479.

14 thms2 active usersReviewed

Machine Learning Operations Research Probability·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 2: Without a Bound on y^NV, Expanding-Projection AIM Has Regret ≤ max{b,h}(T^{δ−1/2} + T^{−1/2} + (y^NV)^{1+2/δ}/T)Research Paper

Motivation

A retailer who restocks a product every period must pick an order-up-to level without knowing the demand distribution. When a period ends with an empty shelf, the retailer records only its sales, so the true demand above the stock level is censored. The classical newsvendor solution, the critical fractile of the demand distribution, cannot be computed. Huh and Rusmevichientong (Math. Oper. Res., 2009) treat this as an online convex optimization problem: the expected one-period cost is convex in the stock level, and its derivative can be estimated without bias from the censored observation alone. Their Adaptive Inventory Management (AIM) algorithm is a projected stochastic subgradient method in the style of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). Its average expected cost converges to the newsvendor cost at rate $O(1/\sqrt T)$ .

That analysis assumes that the manager knows an upper bound $\bar y$ on the newsvendor quantity, and the algorithm projects onto $[0,\bar y]$ . This mission formalizes §3.1 of the paper, which removes the assumption. The projection interval grows with time, and the regret bound is explicit in the unknown newsvendor quantity. Earlier adaptive schemes for censored newsvendor problems include Godfrey and Powell (2001) and Burnetas and Smith (2000).

Setting

Periods are $t = 1, 2, \dots$ . Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with finite mean and distribution function $F$ . Inventory is perishable: every period starts empty, so the stock level is exactly the order-up-to level. With holding cost $h > 0$ per unit left over and shortage cost $b > 0$ per unit of unmet demand, the expected one-period cost at level $y \ge 0$ is

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

The newsvendor quantity is $y^{NV} = \inf\{y \ge 0 : F(y) \ge b/(b+h)\}$ , the minimizer of $Q$ .

Write $\bar B = \max\{b,h\}$ and $P_{[0,a]}(z) = \max\{\min\{z,a\},0\}$ . After period $t$ , the manager observes whether demand fell short of the stock level and forms the signal

H_t(y) = \begin{cases} h, & D_t < y,\\ -b, & D_t \ge y.\end{cases}

Fix $\delta \in (0, 1/2)$ . The modified AIM algorithm starts from a level $\hat y^\delta_1 \in [0,1]$ and updates

\hat y^\delta_{t+1} = P_{[0,\,t^{\delta/2}]}\!\left(\hat y^\delta_t - \epsilon_t H_t(\hat y^\delta_t)\right), \qquad \epsilon_t = \frac{1}{\bar B\sqrt t}.

Neither the step size nor the projection interval uses any bound on $y^{NV}$ . The level $\hat y^\delta_t$ depends only on $D_1, \dots, D_{t-1}$ , and only through the censored observations.

Formalization targets

Goal: Theorem 7 (p. 11)

For every $\delta \in (0, 1/2)$ and every $T \ge 1$ ,

E\left[\frac1T\sum_{t=1}^T Q(\hat y^\delta_t)\right] - Q(y^{NV}) \le \max\{b,h\}\left[\frac{1}{T^{0.5-\delta}} + \frac{1}{T^{0.5}} + \frac{(y^{NV})^{1+2/\delta}}{T}\right].

The bound holds uniformly over all demand laws with finite mean. The price of not knowing $\bar y$ is the slower rate $T^{\delta - 1/2}$ and a transient term in which $y^{NV}$ enters polynomially.

Milestones (proof of Theorem 7, p. 12)

One-step inequality, the instance of Eq. (15) (Appendix A, p. 16) used in the proof. For each $t$ with $y^{NV} \le t^{\delta/2}$ ,

E[Q(\hat y^\delta_t) - Q(y^{NV})] \le \frac{E|\hat y^\delta_t - y^{NV}|^2}{2\epsilon_t} - \frac{E|\hat y^\delta_{t+1} - y^{NV}|^2}{2\epsilon_t} + \frac{\epsilon_t}{2} E|H_t(\hat y^\delta_t)|^2 .

Eq. (10): early rounds, where the projection interval has not yet reached $y^{NV}$ :

E\Big[\sum_{1 \le t \le T,\ t < (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\,(y^{NV})^{1+2/\delta}.

Eq. (11): late rounds:

E\Big[\sum_{1 \le t \le T,\ t \ge (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\, T^{0.5+\delta} + \bar B\, T^{0.5}.

Significance

The result. Theorem 7 shows that a distribution-free, censored-data policy can be asymptotically optimal without any prior bound on the optimal stock level. The only inputs are $b$ , $h$ and the tuning parameter $\delta$ . The explicit constant separates two effects. A transient cost grows with $y^{NV}$ and vanishes like $1/T$ . A steady-state rate $T^{\delta-1/2}$ approaches the known-bound rate $T^{-1/2}$ as $\delta \to 0$ , at the cost of a larger transient. The expanding-projection device applies to other stochastic subgradient methods whose feasible region is unbounded.

Formalizing it. The theorem is proved in the paper, but as far as is known it has no machine-checked proof. The mission produces the modified algorithm as an explicit function of the demand path, the per-step stochastic gradient inequality with a time-varying projection, and the two-phase regret decomposition. The per-step inequality with a varying domain is reusable for other growing-domain online methods.

Difficulty

The standard projected-gradient analysis compares every iterate with a fixed minimizer in a fixed compact set, and it bounds the telescoping distance terms by the diameter of that set. Neither applies here. In the early rounds the projection interval does not contain $y^{NV}$ , so the distance to $y^{NV}$ can grow from step to step. Once the interval contains $y^{NV}$ , the diameter that controls the telescoping sum grows with $t$ . The step sizes and the growing radii must be traded against each other through Abel summation. The bound on $E[H_t(\hat y^\delta_t)(\hat y^\delta_t - y^{NV})]$ needs the conditional-expectation argument that $H_t$ is an unbiased subgradient of $Q$ at a random point independent of $D_t$ . Applying the known-bound theorem with $\bar y$ replaced by $T^{\delta/2}$ does not work, because the algorithm is not given $T$ and the projection radius changes at every step.

Formalization scope

Demand: CappedBaseStock.DemandLaw (a probability law on $\mathbb R_{\ge 0}$ with finite and strictly positive mean) and the i.i.d. path demandPathLaw (Measure.infinitePi), from the published definition CappedBaseStock_Model. The path is zero-based: the paper's $D_t$ is coordinate $t-1$ . The positive-mean field is not needed by Theorem 7. It excludes only $D = 0$ almost surely.
$Q$ and $y^{NV}$ : backorderCost and newsvendorLevel from the published definition LostSalesOrderUpTo.Asymptotic.Backorder. Real levels are passed through Real.toNNReal, and the levels involved are always nonnegative.
The algorithm modAimTarget δ b h ŷ₁ d t is a deterministic recursion on the demand path, and expectations are Bochner integrals over the path measure. All integrands are bounded and measurable, so no non-integrability default enters.
Explicit readings of the paper's loose phrases:
- the first level, which the paper leaves unspecified, is assumed to satisfy $\hat y^\delta_1 \in [0,1]$ ; the theorem fails without it;
- $0 < b$ and $0 < h$ are assumed;
- the sums in (10) and (11) are restricted to $1 \le t \le T$ ;
- when $y^{NV} = 0$ , the sum in (11) starts at $t = 1$ ;
- all powers are real powers, with $0^p = 0$ for $p > 0$ ;
- "the manager does not know any upper bound" is not a hypothesis, because the algorithm uses none.
Trivializing formalizations are ruled out. The statements concern the algorithm's own iterates, not an arbitrary sequence of levels. The constants are the printed ones. The hypotheses are satisfiable, for example with $\hat y^\delta_1 = 0$ .
Useful contributions:
- convexity and Lipschitz continuity of $Q$ with constant $\max\{b,h\}$ ;
- the subgradient identity $E[H_t(y)] = (b+h)F(y^-) - b$ ;
- measurability and boundedness of the iterates;
- independence of $D_t$ from $\hat y^\delta_t$ under the product measure;
- the projected-step inequality.

Selected references

W. T. Huh and 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://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
A. D. Flaxman, A. T. Kalai and H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
G. A. Godfrey and W. B. Powell, An Adaptive, Distribution-Free Algorithm for the Newsvendor Problem with Censored Demands, Management Science 47(8), 2001. https://doi.org/10.1287/mnsc.47.8.1101.10231
A. N. Burnetas and C. E. Smith, Adaptive Ordering and Pricing for Perishable Products, Operations Research 48(3), 2000. https://doi.org/10.1287/opre.48.3.436.12437

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 4: Nonquadratic Multiplier Methods for Inequality Constraints Find an Optimal MultiplierResearch Paper

Motivation

Convex programs with inequality constraints arise when a decision must meet capacity, resource, or performance limits. Their Lagrange multipliers assign a price to each constraint. Finding an optimal multiplier gives a dual certificate and can guide a primal optimization method. Classical quadratic multiplier methods update these prices through a particular penalty. Eckstein's 1993 paper places a broader family of multiplier updates inside the theory of Bregman proximal point algorithms, allowing a nonquadratic function to shape each step (Eckstein 1993, §4.2).

The result here concerns the inequality constrained case, where multiplier vectors must be componentwise nonnegative. Eckstein identifies a monotone conjugate that incorporates this restriction into the primal penalty and proves that the resulting multiplier sequence converges to an optimal multiplier when one exists. The paper also studies primal limit points and the behavior when no optimal multiplier exists (Eckstein 1993, Theorem 7 and proof, pp. 216–219).

Setting

Let $C\subseteq\mathbb R^n$ be closed, nonempty, and convex. Let $f,g_1,\ldots,g_m$ be proper lower semicontinuous convex functions, finite on $C$ . The primal problem is to minimize $f(x)$ over $x\in C$ subject to $g_i(x)\le 0$ for every $i$ . Write $g(x)=(g_1(x),\ldots,g_m(x))$ . A point solves the problem only when it lies in $C$ , satisfies every inequality, and has no larger objective value than any other feasible point.

For a nonnegative multiplier $p$ , the dual functional is $d(p)=\inf_{x\in C}\{f(x)+\langle p,g(x)\rangle\}$ ; it equals $-\infty$ outside the nonnegative orthant. A multiplier $p^*$ is optimal when it maximizes $d$ . The standing assumption that $d$ is not identically $-\infty$ makes this dual functional a meaningful proper concave object (Eckstein 1993, p. 215).

A Bregman function $h$ has an open zone $S$ . It is continuously differentiable there, strictly convex and continuous on $\overline S$ , and satisfies the boundedness and sequential conditions of Definition 1. Its Bregman distance is $D_h(u,v)=h(u)-h(v)-\langle\nabla h(v),u-v\rangle$ , with $u\in\overline S$ and $v\in S$ . The zone contains the strict positive orthant, and the image of its gradient contains that orthant. Its monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$ . Lemma 3 establishes that this function is finite and differentiable everywhere under these assumptions (Eckstein 1993, pp. 205, 215–216).

Given positive step sizes $c_k$ bounded away from zero, recursion (11) chooses $x^{k+1}$ as a minimizer over $C$ of $f(x)+c_k^{-1}h^{*+}(\nabla h(p^k)+c_kg(x))$ , then sets $p^{k+1}=\nabla h^{*+}(\nabla h(p^k)+c_kg(x^{k+1}))$ . The theorem assumes an infinite sequence conforming to these recursions; it does not assert that each minimizer exists for arbitrary data.

Formalization targets

Multiplier convergence

The goal is Eckstein's Theorem 7. If the dual problem has an optimal multiplier, then the multiplier sequence converges to one:

\exists p^*\in\operatorname*{argmax}d\quad\text{such that}\quad p^k\longrightarrow p^*.

When every $g_i$ is continuous on $C$ and $S$ contains the closed nonnegative orthant, each subsequential limit of the primal iterates solves the constrained problem. Under the same zone condition, the multiplier sequence is unbounded if the dual has no optimal multiplier. The printed theorem says “if (10) has no solution” in this last clause; its proof on p. 218 establishes the no-optimal-multiplier condition, which is the version formalized here.

Supporting targets

The milestones include the representations of $h^{*+}$ in Lemma 2, the appendix results governing recession directions and the monotone conjugate, Lemma 3's global finiteness and differentiability, the subdifferential chain rule, and the Bregman proximal point result of Theorem 1. They also capture the paper's claims that recursion (11) is a Bregman proximal point run for $\partial(-d)$ and that primal limit points meet the feasibility, complementarity, and Lagrangian conditions.

Significance

The theorem supplies a convergence guarantee for nonquadratic methods of multipliers with inequality constraints. It separates the dual conclusion, which uses the strict positive orthant condition, from the primal limit and unboundedness conclusions, which additionally require the closed orthant to lie in the zone. This distinction lets a Bregman function whose zone excludes boundary points still yield dual convergence when optimal multipliers exist (Eckstein 1993, Theorem 7, pp. 216–218).

Eckstein proved this theorem on paper. The mission asks for machine checked proofs of its precise statements and the supporting results; the draft statements compile but their proofs remain open. A completed development would also provide reusable finite dimensional infrastructure for extended-real convex functions, monotone conjugates, Bregman distances, and convex-analytic multiplier conditions.

Difficulty

A direct appeal to ordinary proximal point convergence does not identify the update in (11) as a proximal step: the primal minimization uses $h^{*+}$ , whereas the operator of interest is the subdifferential of the negative dual functional. The nonnegative orthant also introduces boundary behavior absent from the equality constrained case. The link requires precise conjugacy and subdifferential statements, including a globally finite monotone conjugate, before Theorem 1 can apply (Eckstein 1993, pp. 215–218). For primal limit points, the issue is to pass from optimality of each primal subproblem to feasibility, complementarity, and minimization of the limiting Lagrangian.

Formalization scope

Lean uses finite dimensional real inner product spaces for the general proximal point theorem and EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) for the primal and multiplier spaces. Functions that the paper regards as extended-valued are represented by EReal; their properness excludes $-\infty$ . The infimum defining $d$ and the supremum defining $h^{*+}$ remain extended-real operations, so an infinite value cannot silently become zero. Real values are extracted from $h^{*+}$ in recursion (11) only because Lemma 3 asserts finiteness everywhere.

The real function $h$ is total in Lean but constrained only on $\overline S$ ; its gradient is evaluated only at points in $S$ . Every multiplier iterate is explicitly in $S$ . The initial primal value $x^0$ is unused by recursion (11). The Bregman proximal point recursion is represented by its equivalent inclusion (4), and a “limit point” is a subsequential limit. The sequential condition (vi) of Definition 1 is stated for $x^k\in\overline S$ , the natural first-argument domain of $D_h$ . The Appendix's essential strict convexity means strict convexity on convex subsets of the subdifferential domain. Its recession direction uses the stated limit inferior condition.

Lemma A4's printed unconditional claim that its composite $G$ is proper lacks a finite-value witness. The formal statement keeps convexity of $G$ unconditional and states properness at a point $x_0$ where all inner functions and the outer function are finite; differentiability of the outer function there is expressed with local finiteness of its extended-real value. At a zero coefficient, its corresponding subgradient term contributes zero without requiring a subgradient to exist. These conditions expose rather than hide the domain issue. The formulation rules out an arbitrary multiplier sequence, an all-space supremum, or a minimization over infeasible points. Contributions proving the milestones, improving shared convex analysis libraries, and checking the boundary conventions are welcome.

Selected references

Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI:10.1287/moor.18.1.202.

15 thms2 active usersReviewed

Dynamic Programming Operations Research·Captain: mikedeng1

Dynamic Pricing and Inventory Control of Substitute Products 1: Under Multinomial Logit Choice the Optimal Dynamic Prices Equalize Marginal RevenuesResearch Paper

Motivation

Retailers selling several related products can change prices as inventory runs down. A sale of one product changes the stock available in later periods, while changing its price also shifts demand toward or away from the other products. Dong, Kouvelis, and Tian study these linked decisions for substitute product variates under a multinomial logit customer choice model. Their 2009 article gives an exact characterization of the optimal dynamic price vector when each in-stock variate can have its own price. The characterization separates a product's inventory opportunity cost from a margin shared across all products, which makes the result more informative than an opaque Bellman maximization.

The mission isolates Theorem 1 of that article. The paper also studies restricted policies that require a unified price or fixed prices for some variates; those results are separate missions in this series. The present target concerns the fully flexible dynamic policy of §3.1, with the model and conventions of §2.

Setting

There are $n$ product variates, indexed by $i$ , with finite quality parameters $a_i$ . Time $t$ is the number of periods remaining, so it counts down to zero. The inventory state $x=(x_i)$ has nonnegative integer coordinates, and $S(x)=\{i:x_i>0\}$ is the set of variates still in stock. At most one customer arrives during a period, with probability $\lambda$ satisfying $0<\lambda\leq1$ . Inventory is not replenished. The retailer chooses a finite, nonnegative price $r_i$ for each in-stock variate. An out-of-stock variate receives the paper's null price and contributes no demand.

An arriving customer chooses among the in-stock variates and the no-purchase option. The multinomial logit model assigns deterministic utility $a_i-r_i$ to variate $i$ and utility $u_0$ to no purchase, with positive scale $\mu$ . Its probabilities are

P_i(x,r)=\frac{\exp((a_i-r_i)/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)},\qquad P_0(x,r)=\frac{\exp(u_0/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)}.

Let $\pi_t(x)$ be the maximum expected revenue from state $x$ with $t$ periods remaining and zero terminal value $\pi_0(x)=0$ . A sale of variate $i$ moves the inventory to $x-e^i$ . Its marginal inventory value is $\Delta^i\pi_t(x)=\pi_t(x)-\pi_t(x-e^i)$ when $i\in S(x)$ . For a continuation value $V$ , the one-period objective is current expected sales revenue plus the expected continuation revenue after a sale or no sale. The Bellman value takes its supremum over all finite nonnegative price vectors. Equation (5) rewrites that objective as $\xi_V(x,r)+V(x)$ , where $\xi_V$ is the probability-weighted marginal revenue.

Formalization targets

Optimal dynamic prices

Theorem 1 asks for a unique common margin $m_t(x)$ satisfying

\left(\frac{m_t(x)}{\mu}-1\right)\exp\left(\frac{m_t(x)+u_0}{\mu}\right) =\sum_{i\in S(x)}\exp\left(\frac{a_i-\Delta^i\pi_{t-1}(x)}{\mu}\right).

For every in-stock variate, the price $r_i^*=\Delta^i\pi_{t-1}(x)+m_t(x)$ must be feasible and attain the Bellman maximum. The margin also satisfies $m_t(x)P_0(x,r^*)=\mu$ . These claims hold for every inventory state, including an empty in-stock set. They are the main target of Theorem 1, equations (9)–(10).

Total expected revenue

For each $s=1,\ldots,t$ , let $m_s(x)$ be the unique margin equation root at the same inventory state $x$ , with $s$ periods remaining. The remaining clause of Theorem 1 states

\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr].

The milestones track the paper's equation (5) and Steps 1–5 of its Appendix A argument: marginal inventory value, the mapping between prices and choice probabilities, concavity in probability coordinates, existence of the margin, optimal choice probabilities, and the one-period value identity.

Significance

The result turns a coupled dynamic program into a precise pricing characterization. It says that differences in optimal prices across products reflect differences in their marginal inventory values; the remaining margin is common. The value identity quantifies the expected revenue earned over the remaining horizon, and the explicit maximizer removes ambiguity about whether the Bellman supremum is attained. These conclusions support the paper's comparisons with restricted pricing policies and its later discussion of how quality and inventory scarcity affect prices Dong, Kouvelis, and Tian (2009).

The result is proved in the article. This mission contributes a Lean statement of the full theorem, its model, and seven named intermediate targets. The draft declarations compile against the pinned Mathlib environment; their proofs remain open. A complete formalization would provide reusable finite MNL choice probabilities, inverse price and probability identities, and a Bellman model for substitute-product inventory. The paper's economic conclusions should be recovered from those formal statements, rather than from a weakened existence claim.

Difficulty

The direct one-period objective in the price vector is not quasiconcave, as the paper notes on p. 323, so a local condition on prices alone does not establish global optimality. The price vector also ranges over an unbounded set, and a supremum could conceal a boundary or attainment issue. Finally, one extra unit of stock changes future probabilities across all products, not just the revenue of that product. These interactions make nonnegative marginal inventory value and the global optimality assertion substantive parts of the result. The probability-space objective is concave on its positive domain, but the printed Appendix A claim of strict concavity on the full domain is stronger than that function permits; uniqueness concerns the normalized choice-probability slice.

Formalization scope

Lean represents products by Fin n, inventories by functions Fin n → ℕ, and time by a natural number counting remaining periods. The model assumes $\mu>0$ and $0<\lambda\leq1$ . The set $S(x)$ filters positive inventory coordinates; an out-of-stock variate is removed from every choice-probability sum, so its null price need not be encoded as a finite real. The objective's no-sale continuation term is counted once, following equations (5) and (22), despite the ambiguous bracket placement in printed equation (3). In-stock prices are finite and nonnegative. Off-stock coordinates of the displayed candidate vector are set to zero and do not affect demand.

Lean's natural-number subtraction in $x-e^i$ is used only for $i\in S(x)$ , where it subtracts exactly one unit. The Bellman value uses a real sSup, whose default on a badly bounded set could otherwise obscure the theorem. The goal and final milestone therefore require an explicit maximizing price vector and equality between the value and its objective. The margin root is stated as unique and every root is covered; it is not hidden behind a choice operator. Equation (11) quantifies over all roots for $s=1,\ldots,t$ at one fixed $x$ , not along a sample path. No assumption that $n>0$ or $S(x)$ is nonempty is added to the goal. The price–probability mapping and interior optimality milestones assume $S(x)$ nonempty where the paper's positive-simplex argument requires it.

A complete development needs finite-sum algebra, real exponential and logarithm facts, concavity on products of real function spaces, and boundedness and attainment facts for the Bellman objective. The MNL probability and inverse-map facts can serve later pricing models; the dynamic value and marginal-stock lemmas serve inventory-control formalizations. Contributions that prove these statements or isolate reusable analytic lemmas are within scope. The statement must retain both the Bellman maximizer and the value identity, so a default sSup value cannot turn the goal into a trivial equality.

Selected references

Lingxiu Dong, Panos Kouvelis, and Zhongjun Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. DOI: 10.1287/msom.1080.0221.

10 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 2: Bregman Proximal Point Sequences Exist When im ∇h Is ℝⁿ, or Is Open and 0 ∈ im TResearch Paper

Motivation

The proximal point method seeks a zero of an operator by repeatedly solving an implicit equation. For a maximal monotone operator, the ordinary quadratic proximal step is available throughout a Hilbert space. Eckstein's 1993 paper replaces the quadratic penalty with a Bregman function, allowing a step to reflect the geometry of a constrained problem. Before convergence can be discussed, each implicit step must have a solution in the region where the Bregman gradient is defined. Eckstein, 1993, §§1–2 isolates that existence question in Theorem 4.

The theorem draws on the L-property and a range theorem attributed to Brézis and Haraux. Their results describe when the image of a sum of monotone operators is large enough to contain the inputs of a proximal step. The paper uses those results to obtain two practical sufficient conditions: a gradient whose image is the whole space, or an open gradient image together with a zero in the image of the operator. Eckstein, 1993, Theorems 2–4

Setting

Let $H$ be a finite-dimensional real inner product space, representing the paper's $\mathbb R^n$ . An operator $T:H\to2^H$ assigns a set of vectors to each point. It is monotone when $\langle x-y,u-v\rangle\ge0$ whenever $u\in Tx$ and $v\in Ty$ , and maximal monotone when its graph cannot be enlarged while preserving monotonicity. Its domain and image are $\operatorname{dom}T=\{x:Tx\ne\varnothing\}$ and $\operatorname{im}T=\{u:\exists x,\ u\in Tx\}$ .

Let $S\subseteq H$ be open. A Bregman function with zone $S$ is a real function $h$ on $\bar S$ satisfying the six conditions of Definition 1: continuous differentiability on $S$ , strict convexity and continuity on $\bar S$ , boundedness of two families of partial level sets, and two sequential conditions that relate convergence to its D-function

D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle,\qquad (x,y)\in\bar S\times S.

The gradient is an operator with domain $S$ and image $\nabla h(S)$ . For positive step sizes $c_k$ , a Bregman proximal point sequence is a sequence $x^k\in S$ satisfying

\frac{1}{c_k}\bigl(\nabla h(x^k)-\nabla h(x^{k+1})\bigr)\in T(x^{k+1})\quad(k\ge0).

This is the inclusion form (4) of recursion (3). The expression $\nabla h+c_kT$ is a sum of set-valued operators, and each step asks for a preimage of $\nabla h(x^k)$ under that sum. Eckstein, 1993, pp. 205–207

Formalization targets

The goal is Theorem 4. If $T$ is maximal monotone, $h$ is Bregman with zone $S\supseteq\operatorname{dom}T$ , and either

\operatorname{im}\nabla h=H, \qquad\text{or}\qquad \operatorname{im}\nabla h\text{ is open and }0\in\operatorname{im}T,

then every $x^0\in S$ and every positive sequence $(c_k)$ admit an infinite Bregman proximal point sequence starting at $x^0$ . The theorem asserts existence for every starting point in the zone, at every step. Eckstein, 1993, p. 209, Theorem 4

The milestones follow the cited results and the paper's proof: trimonotone operators and subdifferentials have the L-property (Theorem 2); the interior and closure of the image of a sum agree with those of the sum of images under the hypotheses of Theorem 3; the subdifferential and gradient sums agree on the domain of $T$ and yield a maximal monotone sum; and the relevant gradient image lies in the image of $\nabla h+cT$ for every $c>0$ . These targets provide the range statement needed for the infinite recursion. Eckstein, 1993, pp. 208–209

Significance

Theorem 4 certifies that the nonlinear proximal point recursion is well defined from any admissible starting point under either range condition. Without this existence statement, a convergence theorem for sequences satisfying the recursion leaves open whether a sequence can be generated. Its range conditions also distinguish Bregman geometries whose gradient covers the whole space from geometries with a smaller but open gradient image. Eckstein, 1993, p. 209

The mathematical result is proved in the paper; the work here is to formalize its definitions, the Brézis–Haraux statements cited there, and the existence theorem in Lean. The milestone statements are open proof obligations in the draft, not claims of completed machine-checked proofs. The operator vocabulary and range theorem can be reused for other implicit algorithms involving sums of monotone operators.

Difficulty

Knowing that $T$ and $\nabla h$ are monotone does not by itself show that a prescribed $\nabla h(x^k)$ belongs to $\operatorname{im}(\nabla h+c_kT)$ . Even maximality of $T$ alone gives no direct description of that image. The hard point is the range of the sum on the zone of $h$ , especially when $\nabla h(S)$ is a proper subset of $H$ . Theorem 3 supplies an interior and closure comparison, but its domain, maximality, and L-property hypotheses must all be established for the particular operators in Theorem 4. Eckstein, 1993, pp. 208–209

Formalization scope

The Lean model uses a finite-dimensional real inner product space $H$ , set-valued operators $H\to\operatorname{Set}H$ , and Mathlib's gradient on the open zone $S$ . The image of $\nabla h$ is precisely $\nabla h(S)$ ; values of the total Lean gradient outside $S$ do not enter it. The function $h:H\to\mathbb R$ is total for Lean's type system, but only values on $\bar S$ matter. Its extension by $+\infty$ outside $\bar S$ is EReal-valued, and the subdifferential uses the published convex-analysis predicate. The L-property uses boundedness below in $\mathbb R$ , matching the paper's strict lower bound above $-\infty$ .

Recursion (3) is represented by its equivalent inclusion (4), with every iterate explicitly in $S$ . The paper leaves the positive step sizes implicit in Theorem 4; the goal quantifies over all such sequences and imposes no convergence-specific lower bound on them. Condition (vi) of Definition 1 is applied to first arguments in $\bar S$ , the stated natural domain of $D_h$ . Trimonotonicity is the three-point cyclic condition used by Brézis and Haraux. A one-step solution, a sequence with an arbitrary starting point chosen by the prover, or an image taken over all of $H$ would not establish this target.

The development needs convex subdifferentials, maximal monotonicity, maximality of appropriate sums, and the Brézis–Haraux range result. Contributions that prove these milestones or add reusable range lemmas are within scope; an optional formalization of the existence part of Theorem 5 is outside the core path.

Selected references

J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI.
H. Brézis and A. Haraux, Image d'une somme d'opérateurs monotones et applications, Israel Journal of Mathematics 23, 165–186, 1976. DOI.

11 thms2 active usersReviewed

Dynamic Programming Operations Research·Captain: mikedeng1

Dynamic Pricing and Inventory Control of Substitute Products 2: The Optimal Unified Dynamic Price under Multinomial Logit ChoiceResearch Paper

Motivation

Retailers often sell several variates of one product (colours, sizes or flavours of an otherwise identical item) from a fixed stock over a short season, with no replenishment. Customers substitute among the variates and the no-purchase option, so the price of one variate changes the demand for all of them, and the stock of each variate changes the value of selling the others. Dong, Kouvelis and Tian (M&SOM 2009) model this joint pricing and inventory problem with multinomial logit (MNL) choice and characterize optimal dynamic prices in closed form up to a scalar equation.

Many sellers do not price variates individually: apparel, sporting goods and airline examples are cited in the paper (Liu and Milner 2006) of unified dynamic pricing, where one price is charged for all variates and changed over time. Proposition 1 of the paper gives the optimal unified price and the optimal revenue in the same form as the paper's main result for variate-specific prices. Comparing the two quantifies how much revenue is lost by restricting to a common price, which is the purpose of the paper's §5.

Setting

There are $n$ variates, $\mathfrak n=\{1,\dots,n\}$ . Variate $i$ has quality index $a_i\in\mathbb R$ , the no-purchase option has utility $u_0\in\mathbb R$ , $\mu>0$ is the MNL scale parameter, and in each period one customer arrives with probability $\lambda\in(0,1]$ . Time $t$ counts the remaining periods, so the season runs $t=T,T-1,\dots,1$ and ends at $t=0$ .

An inventory level is $x\in\mathbb N^n$ . The in-stock set is $S(x)=\{i:x^i>0\}$ , and $x-e^i$ is the inventory after one sale of variate $i\in S(x)$ . Out-of-stock variates are not offered. At the price vector $r$ , an arriving customer buys variate $i\in S(x)$ or nothing with the MNL probabilities

P^i(r)=\frac{e^{(a_i-r^i)/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}},\qquad P^0(r)=\frac{e^{u_0/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}}.

Under unified pricing the decision in each period is one price $r\ge0$ charged for every in-stock variate. The unified value function $\pi_t(x)$ , the maximal expected revenue from $t$ remaining periods, satisfies $\pi_0\equiv0$ and

\pi_t(x)=\max_{r\ge0}\Bigl\{\lambda\sum_{i\in S(x)}rP^i+\lambda\sum_{i\in S(x)}P^i\pi_{t-1}(x-e^i)+(\lambda P^0+1-\lambda)\pi_{t-1}(x)\Bigr\},

with $P^i,P^0$ evaluated at $(r,\dots,r)$ . Write $\Delta^i\pi_{t-1}(x)=\pi_{t-1}(x)-\pi_{t-1}(x-e^i)$ for the marginal value of a unit of variate $i$ , and

\Delta^w\pi_{t-1}(x)=\frac{\sum_{i\in S(x)}e^{a_i/\mu}\Delta^i\pi_{t-1}(x)}{\sum_{i\in S(x)}e^{a_i/\mu}},\qquad a_w=\mu\ln\sum_{i\in S(x)}e^{a_i/\mu}.

Formalization targets

Goal: Proposition 1

For $t\ge1$ and $S(x)\neq\emptyset$ , the equation

\Bigl(\frac{m}{\mu}-1\Bigr)\exp\Bigl(\frac{m+u_0}{\mu}\Bigr)=\exp\Bigl(\frac{a_w-\Delta^w\pi_{t-1}(x)}{\mu}\Bigr)

has a unique solution $m_t(x)$ ; the price

r^*_t(x)=\Delta^w\pi_{t-1}(x)+m_t(x)

is nonnegative and optimal, with $m_t(x)P^0(r^*_t)=\mu$ ; and

\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr],

where $m_s(x)$ solves the equation of period $s$ at the same inventory $x$ . The statement asserts attainment of the maximum, not only a value for $\pi_t$ .

Milestones

The proof in Appendix A proceeds through a one-variable problem. For marginal values $\delta_i$ let $\xi(r)=\sum_{i\in S(x)}\lambda P^i(r)(r-\delta_i)$ . The milestones are: the rewriting (23)–(24) of the optimality equation as an attained $\max_{r\ge0}\xi^u_t+\pi_{t-1}(x)$ ; the derivatives of $P^i$ , $P^0$ and $\xi$ in the common price; the first-order conditions (25)–(26) with $\xi>0$ and $0<P^0<1$ at a stationary point; the second-order condition, giving exactly one stationary point, which is the global maximizer of $\xi$ on $\mathbb R$ ; the formula $r=\delta_w+m$ with $m=\mu/P^0$ and the equation for $m$ ; uniqueness of the root of the margin equation, with root $>\mu$ ; and the displayed revenue sum $\pi_t(x)=\lambda\sum_{s=1}^{t}[m_s(x)-\mu]$ at the same inventory.

Significance

Proposition 1 reduces a dynamic program over a high-dimensional inventory state to a scalar root-finding problem per state and period, and gives the optimal revenue as a sum of margins. It shows that the full dynamic pricing result (Theorem 1 of the paper) survives the restriction to a common price, with the individual marginal values $\Delta^i\pi_{t-1}$ replaced by their quality-weighted average $\Delta^w\pi_{t-1}$ , and the qualities replaced by the aggregate $a_w$ . This is what makes the paper's numerical comparison of unified, static and full dynamic pricing in §5 computable.

The result is proved in the paper; it has not been formalized. A formalization produces a checked version of the MNL derivative calculus, of the quasiconcavity argument for the common-price objective, and of the backward induction, and it closes a step the printed proof leaves implicit: that the maximizer over all real prices is nonnegative, so that it is feasible for the constrained problem.

Difficulty

The one-period objective is not concave in the price, so neither a concavity argument nor a direct appeal to a compactness theorem gives a unique maximizer. Negativity of the second derivative at stationary points is a local statement; the existence of a stationary point and its being the global maximum on all of $\mathbb R$ do not follow from it alone.

The second difficulty is the constraint $r\ge0$ . The paper solves the unconstrained problem. Showing that $\Delta^w\pi_{t-1}(x)+m_t(x)\ge0$ needs a property of the unified value function, nonnegativity of the weighted marginal value, which the paper does not state. The obvious argument, $\pi_{t-1}$ increasing in inventory term by term, does not apply verbatim when a variate leaves the in-stock set, because the choice set itself changes.

Finally, a supremum in Lean is a real number even when not attained; the value identity is only meaningful together with attainment, which the goal states explicitly.

Formalization scope

The model is one definition file, SubstitutePricing.Unified.Model: a structure with $n$ , $a:\mathrm{Fin}\,n\to\mathbb R$ , $u_0$ , $\mu$ , $\lambda$ ; assumptions $\mu>0$ , $0<\lambda\le1$ ; inventories $x:\mathrm{Fin}\,n\to\mathbb N$ ; the in-stock set as a Finset; MNL probabilities with sums over $S(x)$ only (the paper's null price $r^i=\infty$ is modelled by removal from the choice set); and the unified value function by recursion on $t$ , as a real sSup over $r\in[0,\infty)$ . The equation (3) is read with the no-purchase term outside the sum over variates, as the paper's (5) and (22) use it.

Committed conventions and restrictions:

$t\ge1$ in Proposition 1 (the printed " $t=T,\dots,0$ " includes $t=0$ , where $\pi_{t-1}$ does not exist).
$S(x)\neq\emptyset$ in every statement of the dynamic program and in the static milestones that use it: for an empty in-stock set $a_w$ and $\Delta^w\pi$ involve $\ln0$ and $0/0$ , and the revenue formula fails.
The optimal margin is quantified as the unique root of its equation, and the revenue formula takes the roots of all periods $s\le t$ at the same inventory $x$ .
The goal asserts nonnegativity of $r^*_t$ ; the paper's proof uses but does not prove it.
The paper's intermediate display (27) is misprinted and is not formalized; its correct consequences are.
Milestones 2–6 concern a static objective with arbitrary marginal values $\delta$ ; only the goal and the recursion milestone refer to the value function.

A statement about $\pi_t$ alone, without the attainment and feasibility of $r^*_t$ , would be trivially satisfiable by a junk supremum and is ruled out by the goal's form.

Infrastructure needed: derivatives of MNL probabilities, a quasiconcavity or unique-critical-point lemma for one-variable functions, a root lemma for $(m/\mu-1)e^{(m+u_0)/\mu}$ , and a monotonicity property of the unified value function. The MNL derivative calculus and the root lemma are reusable for the companion missions on full dynamic pricing and mixed pricing from the same paper. Contributions on any milestone, and on the nonnegativity of $\Delta^w\pi_{t-1}$ , are welcome.

Selected references

L. Dong, P. Kouvelis, Z. Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. https://doi.org/10.1287/msom.1080.0221
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997. https://doi.org/10.1287/opre.45.1.24
Q. Liu, J. Milner, Multiple-item dynamic pricing under a common pricing constraint, working paper, University of Toronto, 2006 (cited in the source as the motivation for unified pricing).
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.

9 thms2 active usersReviewed

Algorithmic Game Theory Convex Optimization Operations Research·Captain: mikedeng1

Cooperative Fuzzy Games 4: The Fuzzy Core of an Exchange Economy Coincides with Its Set of Walras EquilibriaResearch Paper

Motivation

The core of an exchange economy is the set of allocations that no group of consumers can improve upon by trading only among themselves. The Walras equilibria (competitive equilibria) are the allocations supported by a price system at which every consumer maximizes preference on a budget set. Every Walras equilibrium is in the core, but for a fixed finite economy the core is usually much larger. Edgeworth (1881) conjectured that the core shrinks to the competitive allocations as the number of traders grows; Debreu and Scarf (1963) proved this for replica economies, and Aumann (1964) proved exact equality for an atomless continuum of traders.

Jean-Pierre Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6 (1981) 1–13) gives a third route to the same conclusion, with a fixed finite number of consumers. Coalitions are allowed to be fuzzy: a consumer may join with any rate of participation between 0 and 1. Once all fuzzy coalitions may block, the core of the economy, now called the fuzzy core, is exactly the set of Walras equilibria (Theorem 4.1, p. 6). The paper presents this as a slight modification of the Debreu–Scarf theorem; in Remark 4.2 it observes that Debreu–Scarf's replica coalitions correspond to the rational points of the cube $[0,1]^n$ .

This mission formalizes §4 of the paper. It is the fourth mission of a series on the paper; the others treat the cores of fuzzy games with and without side payments and the values of smooth fuzzy games.

Setting

There are $n$ consumers $i \in N = \{1,\dots,n\}$ and $l$ commodities. Consumer $i$ consumes bundles in $\mathbb{R}^l_+$ , ranks them by a preference relation $\succcurlyeq_i$ (with strict part $\succ_i$ ), and owns a set $Y(i) \subset \mathbb{R}^l$ of possible initial endowments. Each $Y(i)$ is closed, convex and comprehensive: whenever $y \in Y(i)$ and $z \ge 0$ , also $y - z \in Y(i)$ .

A fuzzy coalition is a vector $\tau \in [0,1]^n$ ; $\tau_i$ is the rate at which consumer $i$ participates, and $A_\tau = \{i : \tau_i > 0\}$ is the set of participants. The coalition $\tau$ disposes of the endowments

Y(\tau) = \sum_{i \in N} \tau_i\, Y(i),

and its allocations are the families $x_\tau = (x_\tau^i)_{i \in A_\tau}$ of bundles $x_\tau^i \in \mathbb{R}^l_+$ with $\sum_i \tau_i x_\tau^i \in Y(\tau)$ ; this set is $X(\tau)$ . The allocations of the whole economy are $X(N) = X(\tau^N)$ , $\tau^N = (1,\dots,1)$ .

An allocation $x \in X(N)$ is in the fuzzy core if there is no nonzero fuzzy coalition $\tau$ and allocation $x_\tau \in X(\tau)$ with $x_\tau^i \succ_i x^i$ for every $i \in A_\tau$ .

The income of consumer $i$ at prices $p \in \mathbb{R}^l$ is $r_i(p) = \sup_{y \in Y(i)} p\cdot y$ , and the budget set is $B_i(p) = \{x \in \mathbb{R}^l_+ : p \cdot x \le r_i(p)\}$ . An allocation $\bar x \in X(N)$ is a Walras equilibrium if some price $\bar p \in \mathbb{R}^l$ satisfies, for every $i$ ,

\bar p \cdot \bar x^i = r_i(\bar p) \qquad\text{and}\qquad \bar x^i \succcurlyeq_i x \ \text{ for all } x \in B_i(\bar p).

Assumption (1) of §4 requires each preference to be continuous and convex, with $x \succ_i y \Rightarrow \alpha x + (1-\alpha) y \succ_i y$ for $\alpha \in\, ]0,1[$ ; no consumer to be satiated; and each $Y(i)$ to contain a vector with all coordinates strictly positive.

Formalization targets

Goal: Theorem 4.1

Under assumption (1),

\text{fuzzy core} \;=\; \{\text{Walras equilibria}\}.

Milestones, from the proof of Theorem 4.1

Every Walras equilibrium belongs to the fuzzy core.
For an allocation $\bar x \in X(N)$ , each set $Q(i) = Y(i) - \{x \in \mathbb{R}^l_+ : x \succ_i \bar x^i\}$ is nonempty.
If $\bar x$ belongs to the fuzzy core, then

0 \notin \operatorname{co}\Big(\bigcup_{i=1}^n Q(i)\Big).

The remaining step of the paper, from milestone 3 to the existence of the equilibrium price, is stated there only as "by known arguments" and is left to the solver as part of the goal.

Significance

The result. Theorem 4.1 is a core equivalence theorem for an economy with finitely many consumers and no replication or continuum of traders. It identifies the competitive allocations as exactly the allocations that are stable against partial coalitions. It also makes visible which coalitions matter: Remark 4.1 attributes the equivalence to the fact that all fuzzy coalitions are allowed to form, so that the set of coalitions is convex. The same fuzzy-coalition device underlies the nonemptiness results for cores of fuzzy games in §5–§7 of the paper.

Formalizing it. The theorem is proved in the paper, in one paragraph that defers its final step to "known arguments". To our knowledge neither the theorem nor the Debreu–Scarf or Aumann core equivalence theorems have been formalized in Lean. A complete development provides a reusable model of an exchange economy with preference relations and comprehensive endowment sets, a checked argument from separation to equilibrium prices, and a template for the classical core equivalence theorems.

Difficulty

The inclusion of the Walras equilibria in the fuzzy core is a budget computation. The converse is the content of the theorem: from the mere absence of improving fuzzy coalitions, a single price vector must be produced that works for all consumers simultaneously. Separating consumer by consumer gives one price per consumer, not a common one, so the coalitional structure has to enter before any price exists. Once a candidate price is available, it still has to be shown nonnegative, each equilibrium bundle has to exhaust its owner's income, and no bundle in a budget set may be strictly preferred; each of these uses a different part of assumption (1), and the paper leaves all three to "known arguments". The incomes $r_i(p)$ may be $+\infty$ for prices with negative coordinates, so finiteness at the equilibrium price is part of the conclusion, not an assumption.

Formalization scope

Consumers are Fin n, commodities Fin l; an allocation is a function Fin n → Fin l → ℝ, a price a vector Fin l → ℝ, and $p \cdot y = \sum_k p_k y_k$ . A single definitions file (FuzzyGames.Walras.Basic) holds the economy, its assumptions, $Y(\tau)$ , $X(\tau)$ , the fuzzy core, incomes, budget sets, Walras equilibria and the sets $Q(i)$ .

The formalization commits to the following readings, each recorded in the items' Formalization Notes:

Complete preferences. The paper's "preference preordering" is read, as in Debreu's usage, as a reflexive, transitive and complete relation on $\mathbb{R}^l_+$ . The relation is a predicate on $\mathbb{R}^l$ , but every assumption and every use is restricted to $\mathbb{R}^l_+$ .
Continuity means closed upper and lower contour sets in $\mathbb{R}^l_+$ ; convexity means convex upper contour sets, plus the condition of (1)(i).
Assumption (1)(i) is printed with $x \succcurlyeq y$ in the premise, which fails at $x = y$ ; it is stated with $x \succ y$ .
Blocking is strict and by nonzero coalitions. The fuzzy-core definition is printed with $x_\tau^i \succcurlyeq x^i$ ; the proof uses $\succ$ , and the weak version would let every allocation block itself. The coalition $\tau = 0$ is excluded, since its condition over $A_\tau = \emptyset$ is vacuous.
Dummy coordinates. An allocation of $\tau$ is a full family of $n$ bundles; those with $\tau_i = 0$ are multiplied by $0$ , unconstrained and never compared.
$Y(\tau)$ is Mathlib's pointwise Minkowski sum of scaled sets.
Incomes take values in the extended reals (EReal), so that $r_i(p) = +\infty$ is represented and never replaced by a default value.

A trivializing formalization is ruled out: the assumptions are satisfiable, and a sorry-free check (one consumer, one commodity, $x \succcurlyeq y \iff x \ge y$ , $Y(1) = (-\infty, 1]$ ) verifies them together with a Walras equilibrium, so neither side of the goal is empty by construction.

Contributions welcome: proofs of the milestones, a separation-to-prices lemma for comprehensive endowment sets, and general facts about complete continuous convex preferences on $\mathbb{R}^l_+$ , which are reusable for any general equilibrium development.

Selected references

J.-P. Aubin, Cooperative fuzzy games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
G. Debreu, H. Scarf, A limit theorem on the core of an economy, International Economic Review 4(3) (1963) 235–246. https://doi.org/10.2307/2525290
R. J. Aumann, Markets with a continuum of traders, Econometrica 32 (1964) 39–50. https://doi.org/10.2307/1913732
G. Debreu, Theory of Value, Cowles Foundation Monograph 17, Yale University Press, 1959.

6 thms2 active usersReviewed

Completed

Dynamic Programming Linear Optimization Operations Research·Captain: mikedeng1

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 2: The Greedy Forward Dual Solution Is Optimal and Its Value Is the Lot-Sizing CostResearch Paper

Motivation

Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).

The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.

Setting

There are periods $1,\ldots,n$ . Demand $d_t$ and setup cost $f_i$ are nonnegative for the periods in the horizon. The marginal production cost $c_i$ is any real number. Write $d_{i,j}=\sum_{t=i}^j d_t$ for cumulative demand from $i$ through $j$ . Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods $1,\ldots,n$ .

The forward lot-sizing cost $F(j)$ describes the least cost of serving periods $1,\ldots,j$ under the zero-inventory property cited by the paper. Its recursion starts with $F(0)=0$ . If $d_j=0$ , no new production is needed and $F(j)=F(j-1)$ . If $d_j>0$ , the last production setup may occur at some $i\le j$ , giving

F(j)=\min_{1\le i\le j}\bigl(f_i+c_i d_{i,j}+F(i-1)\bigr).

This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at $d_j=0$ would charge a setup that need not occur.

Program D′ chooses free real values $v_1,\ldots,v_n$ to maximize $\sum_{t=1}^n d_tv_t$ , subject to

\sum_{t=i}^n d_t\max\{0,v_t-c_i\}\le f_i \qquad(1\le i\le n).

“Free” means there is no nonnegativity constraint on $v_t$ . The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.

The greedy forward rule visits periods in increasing order. At a period with $d_j>0$ , the chosen value is the minimum of the upper bounds left by the constraints indexed $i\le j$ :

v_j=\min_{1\le i\le j} \left(c_i+\frac{f_i-\sum_{t=i}^{j-1}d_t\max\{0,v_t-c_i\}}{d_j}\right).

When $d_j=0$ , the rule places no restriction on $v_j$ . This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.

Formalization targets

The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:

\sum_{t=1}^j d_tv_t=F(j)\quad(1\le j\le n), \qquad \sum_{t=1}^n d_tu_t\le\sum_{t=1}^n d_tv_t \quad\text{for every feasible }u.

The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.

Significance

The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost $F(n)$ , and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to $F$ Wagelmans et al., p. S153.

A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.

Difficulty

A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with $F(j)$ also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.

Formalization scope

Lean represents the horizon by natural-number indices $1,\ldots,n$ and the demand, setup, marginal-cost and dual sequences by functions $\mathbb N\to\mathbb R$ . Finite sums use closed intervals; the sum before period $j$ uses $[i,j)$ , so it is empty when $i=j$ . Minima are over the nonempty finite set $\{1,\ldots,j\}$ , only when $j\ge1$ . The horizon $n=0$ has empty sums and no constraints. The cost and dual values are real, with no sign condition on $c_i$ or $v_i$ .

Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through $n$ holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.

The identification of $F$ with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including $O(n^2)$ for the greedy forward algorithm and $O(n\log n)$ for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of $F$ as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.

Selected references

A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1, 1992, S145–S156. DOI

7 thms2 active usersReviewed

Computational Geometry Dynamic Programming Operations Research·Captain: mikedeng1

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 1: The Threshold Rule on Efficient Periods Picks an Optimal Next Production PeriodResearch Paper

Motivation

Economic lot sizing asks how to meet a known sequence of demands while deciding when to set up production and how much to carry forward. It is a basic deterministic inventory problem: a setup has a fixed cost, production has a per-unit cost, and inventory may be held for later demand. Recomputing every possible next production period in the standard backward dynamic program takes a quadratic number of candidate comparisons. Wagelmans, Van Hoesel and Kolen use the geometry of cumulative-demand points to identify which candidates can affect the minimum. Their Section 2 gives the threshold rule targeted here. Wagelmans, Van Hoesel and Kolen (1992)

The paper notes independent related work by Aggarwal and Park and by Federgruen and Tzur. The published Prove2Me items for Federgruen and Tzur formalize a forward recursion and its minimal optimal predecessor lists. They address the same planning problem through different state variables; the backward value and efficient periods of this mission are new objects. Wagelmans, Van Hoesel and Kolen (1992), p. S145

Setting

A planning horizon consists of periods $1,\dots,n$ , with $n\ge1$ , and an extra terminal period $n+1$ . In period $i$ , a known demand $d_i\ge0$ must be met without backlogging. The final demand is positive, $d_n>0$ ; a trailing zero-demand period could otherwise be deleted. A production setup costs $f_i\ge0$ , and every unit produced in that period has a marginal cost $c_i\in\mathbb R$ . The sign of $c_i$ is unrestricted. Holding costs have been absorbed into these transformed marginal costs, as in Section 1 of the paper. Define the remaining demand $D(t)=\sum_{j=t}^{n}d_j$ , with $D(n+1)=0$ . If production at $i$ covers demand until the next production period $t$ , then $D(i)-D(t)$ units are produced. Wagelmans, Van Hoesel and Kolen (1992), pp. S146–S147

The backward value $G(t)$ starts at $G(n+1)=0$ and follows Equation (1). At positive demand, it minimizes $f_i+c_i[D(i)-D(t)]+G(t)$ over $i<t\le n+1$ . When $d_i=0$ , skipping setup and using $G(i+1)$ is an additional choice. The paper identifies $G(t)$ with the optimal cost from $t$ onward using the cited zero-inventory property. This mission takes Equation (1) as the definition of $G$ ; it does not formalize the separate equivalence with the original production-plan formulations. Wagelmans, Van Hoesel and Kolen (1992), p. S147

For a fixed $i$ , plot the finite points $(D(t),G(t))$ for $i<t\le n+1$ . Their lower convex envelope is a piecewise linear graph. Its endpoints and places where its slope changes are breakpoints; the corresponding period indexes form the efficient set $E_i$ . Write $\operatorname{succ}_i(t)$ for the next larger index in $E_i$ . The consecutive-point ratio is $r_i(t)=[G(t)-G(\operatorname{succ}_i(t))]/[D(t)-D(\operatorname{succ}_i(t))]$ . These objects have no optimization over production policies hidden in their definitions. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization targets

Efficient candidates

Proposition 1 says every candidate outside $E_i$ can be removed without changing the minimum:

\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=\min_{t\in E_i}\{c_i[D(i)-D(t)]+G(t)\}.

The endpoint and slope claims establish the geometry used in this reduction. Proposition 2 compares neighboring efficient periods using $r_i(t)$ and $c_i$ . Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S149

Threshold rule and backward value

The selected period is the first efficient index whose ratio falls below the current marginal cost, with the terminal period as fallback:

q(i)=\min\bigl(\{n+1\}\cup\{t\in E_i:t<n+1,\ r_i(t)<c_i\}\bigr).

The goal asserts that the full candidate minimum is attained there and that the algorithm's resulting assignment equals $G(i)$ :

\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=c_i[D(i)-D(q(i))]+G(q(i)),

G(i)=\begin{cases}f_i+c_i[D(i)-D(q(i))]+G(q(i)),&d_i>0,\\ \min\{G(i+1),f_i+c_i[D(i)-D(q(i))]+G(q(i))\},&d_i=0.\end{cases}

This states the mathematical choice and value; it does not assert a time bound. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S150

Significance

The result reduces a finite dynamic-programming minimum to the vertices of a lower envelope and gives an explicit threshold for choosing a minimizing vertex. It explains which future production period the backward recursion may select even when marginal costs are negative or some intermediate demands are zero. The paper uses ordered slopes to implement the selection efficiently; a solver proving the statements here establishes the mathematical correctness of that selection independently of a particular list representation. Wagelmans, Van Hoesel and Kolen (1992), pp. S148–S150

The paper's result is proved in print. The Lean statements are open proof obligations in this proposal. A complete development would add reusable finite lower-envelope facts, including vertex dominance and the order of adjacent slopes, as well as a machine-checked treatment of the zero-demand tie convention. The previously published forward-algorithm items do not supply these backward-recursion facts.

Difficulty

A candidate point can have a smaller value $G(t)$ than a neighboring point yet still fail to minimize $c_i[D(i)-D(t)]+G(t)$ for a given $c_i$ . Comparing raw values alone therefore cannot identify the selected period. The lower envelope must retain exactly the points that can support a line of slope $c_i$ , and their consecutive ratios must be ordered. Zero demand creates repeated abscissae; without a representative rule, a ratio may have denominator zero and the successor is ambiguous. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization scope

Periods are natural numbers starting at $1$ ; $n+1$ is the terminal sentinel. Demands, setup costs, marginal costs and values are real numbers. Finite minima use attained Finset.inf', with nonempty domains. The effective score omits the common setup cost $f_i$ . No sign restriction is imposed on $c_i$ . The efficient set is determined by a finite chord test for lower-envelope vertices: points on a chord are excluded, and at identical abscissa and height the earliest period is retained. This makes explicit the paper's zero-demand replacement convention on p. S150. The successor is used only on nonsentinel efficient periods; there its denominator is positive. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

The algorithm's printed Iterations use $d_{1n}$ where $d_{in}$ is required; the Lean statement uses $D(i)-D(q(i))=d_{i,q(i)-1}$ , matching the preceding display and the numerical table. The zero-demand branch explicitly includes skipping setup. The selector is the ratio-threshold rule, rather than an argmin, and the efficient set is the actual lower-envelope vertex set rather than all periods. A finite zero-demand example and Tables I–II are used as verification data. The paper's $O(n\log n)$ bound, the binary-search implementation, the amortized list updates, the $O(n)$ Wagner–Whitin specialization and the final production-plan construction are outside this mission: they require additional algorithm-state and cost-model statements. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S152

Selected references

A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1 (1992), S145–S156. DOI: 10.1287/opre.40.1.S145

8 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Negative Dynamic Programming IV: Switching at Each Stage to the Policy with the Better Continuation Return Does at Least as Well as Both PoliciesResearch Paper

Motivation

Policy improvement is one of the two classical ways of solving a Markov decision problem: start from a policy, compute its return, and change the decision wherever another action looks better against that return. Howard (1960, Dynamic Programming and Markov Processes) introduced it for finite state and action spaces, and Blackwell (1965) proved it for discounted problems on Borel spaces. A related routine combines two given policies instead of improving one: at each state, follow whichever policy has the larger return there. Eaton and Zadeh (1962, J. Basic Eng. Ser. D 84, 23–29) proved that this combination of two stationary policies is at least as good as both in the negative case with finite state and action spaces (as credited on p. 889 of Strauch's paper).

Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966) 871–890) treats the negative case: all one-stage returns are non-positive (costs) and there is no discounting. This case covers stochastic shortest-path and optimal-stopping problems with positive costs, where expected total returns may be $-\infty$ and the contraction arguments of the discounted case are not available. Section 9 of the paper shows that both improvement routines remain valid there, for arbitrary randomized history-dependent policies on Borel spaces, and that they fail in the positive case (Examples 4.2 and 9.1 of the paper).

Timeline:

1960, Howard: policy iteration for finite state and action spaces.
1962, Eaton and Zadeh: the two-policy combination for finite negative problems.
1965, Blackwell: both routines for discounted problems with Borel state and action spaces.
1966, Strauch, §9: Howard's routine (Theorem 9.2), the history-dependent switching theorem (Theorem 9.3) and its Markov and stationary forms (Corollaries 9.1, 9.2) in the negative case on Borel spaces.

Setting

The state space $S$ and the action space $A$ are non-empty Borel sets. The law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ , and the return $r(s,a,t)$ is a Borel function with $-\infty<r\le 0$ whose one-step expectation $\int r(s,a,t)\,q(dt\mid s,a)$ is finite at every $(s,a)$ . There is no discounting ( $\beta=1$ ).

A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the $n$ -th action $a_n$ from a probability kernel $\pi_n(\cdot\mid h)$ that may depend on the whole history $h=(s_1,a_1,\dots,a_{n-1},s_n)$ . The expected return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\pi_1q\cdots\pi_nqr\,(s)\in[-\infty,0],

the sum of the expected one-stage returns. For a terminal reward $w\le 0$ that depends on the history $(s_1,a_1,\dots,s_{n+1})$ , $I_n(\pi,w)$ is the expected return of following $\pi$ for $n$ stages and then receiving $w$ .

Given two policies $\sigma$ and $\tau$ , their continuation returns at a history $h=(s_1,\dots,s_n)$ are

u_n(h)=\sum_{j=n}^{\infty}\sigma_nq\cdots\sigma_jqr\,(h),\qquad v_n(h)=\sum_{j=n}^{\infty}\tau_nq\cdots\tau_jqr\,(h),

the expected returns from stage $n$ on if $\sigma$ , respectively $\tau$ , is used from $h$ on with its own kernels fed the full history. The switching policy $\pi$ uses $\sigma_n$ on $B_n=\{u_n>v_n\}$ and $\tau_n$ on its complement. In Lean these objects are contReturn, IsSwitch, wmax (for $w_n=\max(u_n,v_n)$ ), InH (for $I_n(\pi,w)$ ) and I, in the namespace NegativeDP.Switching.

Formalization targets

Goal: Theorem 9.3 (negative case)

For all policies $\sigma,\tau$ , the switching rule defines a policy $\pi$ , and every such $\pi$ satisfies

I(\pi)\ge\max\big(I(\sigma),I(\tau)\big)\quad\text{at every initial state.}

Milestones (proof of Theorem 9.3, p. 888)

With $w_n=\max(u_n,v_n)$ and $\pi$ the switching policy:

I_0(\pi,w_1)=w_1=\max(I(\sigma),I(\tau)),

w_n=\pi_n(r+u_{n+1})\text{ on }B_n,\qquad w_n=\pi_n(r+v_{n+1})\text{ on }B_n^c,

w_n\le\pi_n(r+w_{n+1}),\qquad I_{n-1}(\pi,w_n)\le I_n(\pi,w_{n+1}),\qquad I_{n-1}(\pi,w_n)\ge\max(I(\sigma),I(\tau)).

Further results (not milestones)

Theorem 9.2 (Howard): if $I(f,\pi)\ge I(\pi)$ then $I(f^{(\infty)})\ge I(\pi)$ . Corollary 9.1: the switching theorem for Markov policies, comparing $I(^{n-1}\sigma)$ and $I(^{n-1}\tau)$ at the current state. Corollary 9.2 (Eaton–Zadeh): for stationary $f^{(\infty)},g^{(\infty)}$ , the rule $h=f$ where $I(f^{(\infty)})\ge I(g^{(\infty)})$ and $h=g$ elsewhere satisfies $I(h^{(\infty)})\ge\max(I(f^{(\infty)}),I(g^{(\infty)}))$ .

Significance

Theorem 9.3 yields an improvement step that needs only the returns of two policies, not an optimality equation or a value function. Its Markov and stationary forms give policy-combination results usable for stochastic shortest-path and positive-cost problems, and together with Theorem 9.2 they justify policy-iteration schemes in the negative case on general state spaces. Example 9.1 of the paper shows that no comparable routine exists in the positive case, so the sign assumption is essential.

The results are proved in the paper. No machine-checked version of any of them exists, for the negative case or on Borel spaces; the related items on Prove2Me treat finite or discounted models. This mission produces the statements in Lean over Blackwell's published model of history-dependent plans, a construction of continuation returns from an arbitrary history, and terminal rewards that depend on the whole history.

Difficulty

The argument of the discounted case, which passes to the limit through the vanishing tail $\beta^n w_n$ , is not available: with $\beta=1$ the terminal term does not vanish, and returns may be $-\infty$ . Comparing $u_n$ and $v_n$ at the current state only is not enough either: for history-dependent policies the continuation returns depend on the whole history, and the switching set $B_n$ must be shown to be Borel in the history before the switching rule is even a policy. The induction also requires integrating extended-real terminal rewards against the history law and identifying the integral of the one-step operator with the next-stage expected return.

Formalization scope

Borel sets are non-empty standard Borel types; Baire functions are measurable functions. Policies are Blackwell's DiscountedDP.Stationary.Plan (one Markov kernel per decision, on Hist S A n). Decisions are numbered from $0$ in Lean, so Lean's index $n$ is the paper's stage $n+1$ .
Only the negative case is formalized ( $r\le0$ real-valued, $q$ -integrable at every $(s,a)$ , $\beta=1$ ). The paper states Theorem 9.3 for the discounted and negative cases; the discounted case is not part of this mission.
Returns lie in $[-\infty,0]$ and are EReal values computed as minus the lintegral of the loss $-r$ ; Bochner integrals and toReal are never used, so a return of $-\infty$ is not silently turned into $0$ . $I(\pi)$ is the sum of stage expectations, equal to $e_\pi\rho$ by monotone convergence.
Terminal rewards are read through their negative parts; they are applied only to $w_n\le 0$ .
The switching policy is characterized by the predicate IsSwitch, not constructed. A statement "every switching policy satisfies the bound" would hold vacuously if no plan satisfied the rule; the goal therefore also asserts that a switching plan exists, which is the content of the paper's "define $\pi$ by". The same pattern is used in Corollaries 9.1 and 9.2 (the rule defines a measurable decision rule).
Ties $u_n=v_n$ go to $\tau$ in Theorem 9.3, and $I(^{n-1}\sigma)=I(^{n-1}\tau)$ to $g_n$ in Corollary 9.1 (strict $>$ as printed); in Corollary 9.2 ties go to $f$ (non-strict $\ge$ as printed).
Lemma 3.1 ( $I_n(\pi,0)\downarrow I(\pi)$ ), used in the last step of the proof, is posed in mission I of this series and not repeated here.

Contributions welcome: measurability of continuation returns in the history (needed for the existence part), the identification of the history law with the continuation law from the initial state, and a Chapman–Kolmogorov identity for the continuation kernels. These are reusable in any development on history-dependent policies over Borel spaces.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
J. H. Eaton and L. A. Zadeh, Optimal pursuit strategies in discrete-state probabilistic systems, J. Basic Eng. Ser. D 84 (1962) 23–29 (reference [7] of Strauch's paper).
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.

9 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.

A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.

Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.

Setting

A negative dynamic programming problem consists of non-empty Borel sets $S$ (states) and $A$ (actions), a law of motion $q(\cdot\mid s,a)$ , which is a probability kernel from $S\times A$ to $S$ , and a Borel return function $r(s,a,t)$ with

r\le 0,\qquad r>-\infty,\qquad \int r(s,a,t)\,dq(t\mid s,a)>-\infty\ \ \text{for all }(s,a).

There is no discounting. A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the action $a_n$ at stage $n$ from a probability kernel $\pi_n(\cdot\mid h_n)$ , where $h_n=(s_1,a_1,\dots,a_{n-1},s_n)$ is the history. A policy is Markov if $a_n=f_n(s_n)$ for Borel maps $f_n:S\to A$ , semi-Markov if $a_n=g_n(s_1,s_n)$ for Borel $g_n$ , and stationary, written $f^{(\infty)}$ , if $a_n=f(s_n)$ for one Borel rule $f$ . Random Markov and random semi-Markov policies draw $a_n$ from kernels in $s_n$ , respectively $(s_1,s_n)$ .

The expected total return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\mathbb E^{\pi}_{s}\,r(s_n,a_n,s_{n+1})\in[-\infty,0],

the optimal return is $v^*(s)=\sup_\pi I(\pi)(s)$ over all policies, and $\pi^*$ is optimal if $I(\pi^*)(s)\ge v^*(s)$ for every $s$ . For a Borel rule $f$ , the operator $T$ acts on non-positive Borel functions $u$ by

Tu(s)=\int r(s,f(s),t)+u(t)\,dq(t\mid s,f(s)).

The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

\big(\exists\,\pi^*\ \ I(\pi^*)\ge v^*\big)\ \Longrightarrow\ \exists\,f\ \text{Borel},\ \ I(f^{(\infty)})\ge v^* .

Milestones

Lemma 2.1: for a kernel $q(\cdot\mid x)$ and a Borel $u\le 0$ on $X\times Y$ there is a Borel $f$ with $u(x,f(x))\ge\int u(x,y)\,dq(y\mid x)$ .
Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$ .
Lemma 4.1 (a), (b): policies built from the conditional laws of $a_n$ given $(s_1,s_n)$ , respectively given $s_n$ under an initial law $p$ , reproduce the laws of $(s_1,s_n,a_n,s_{n+1})$ , respectively the $p$ -averaged laws of $(s_n,a_n,s_{n+1})$ .
Theorem 4.1: for every policy $\pi$ and initial law $p$ there are a random semi-Markov $\pi^*$ and a random Markov $\pi^{**}$ with $I(\pi)=I(\pi^*)$ and $pI(\pi)=pI(\pi^{**})$ for every return function.
Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$ , then $I(\pi)\ge I(\sigma)$ .
Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$ .
Theorem 5.1 (N), parts (a)–(g): the properties of $T$ , including $TI(\pi)=I(f,\pi)$ , $TI(f^{(\infty)})=I(f^{(\infty)})=\lim_n T^n0$ and $I_n(\pi,v)=T_1\cdots T_nv$ for Markov $\pi$ .

Significance

Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on $(p,\varepsilon)$ -optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.

All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.

Difficulty

The obvious argument starts from an optimal $\pi^*$ , takes its first decision rule $f$ , and shows that $f^{(\infty)}$ is optimal. That fails for a general $\pi^*$ , because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal $-\infty$ , and every limit exchange has to respect that.

Formalization scope

Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return $r$ is real-valued, non-positive and integrable under $q(\cdot\mid s,a)$ for every $(s,a)$ . Returns live in the extended reals. $I(\pi)$ , $I_n(\pi,v)$ , $T$ and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in $[0,\infty]$ , so a return of $-\infty$ is never collapsed to $0$ . $I(\pi)$ is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. $v^*$ is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case ( $r\le 0$ , $\beta=1$ ) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.

Explicit choices:

Lean numbers decisions from $0$ . Hist S A n is the paper's $H_{n+1}$ and the plan's kernel κ n is $\pi_{n+1}$ .
The objects $\pi^*$ and $\pi^{**}$ of Lemma 4.1 are defined in the paper's proof as conditional distributions. Here their defining property is a hypothesis: for every initial state, or after averaging over $p$ , the joint law of $(s_n,a_n)$ is the law of $s_n$ followed by the kernel.
In Theorem 4.1, "for any return function $r$ " is a quantifier over every negative problem with the same law of motion, placed after the choice of $\pi^*$ and $\pi^{**}$ .
In Theorem 5.1 (b), $u+c$ is required to lie in $M(S)$ . In (d), the increasing part holds only on $\{\sup_jTu_j>-\infty\}$ .
In Theorem 5.1 (f), $T$ is applied to $I(\pi)$ for a general plan with no measurability hypothesis. The lower integral is defined for every function.

Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell and C. Ryll-Nardzewski, Non-existence of everywhere proper conditional distributions, Ann. Math. Statist. 34(1) (1963) 223–225. https://doi.org/10.1214/aoms/1177704259

16 thms2 active usersReviewed

Completed

Analysis Operations Research·Captain: mikedeng1

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

In 1950 the United States Supreme Court appeared to be moving toward treating corporate integration, horizontal or vertical, as illegal per se under the antitrust laws. Joseph J. Spengler's note in the Journal of Political Economy argued that this conflates two different things: horizontal integration can suppress competition, but vertical integration, the joining of successive stages of production under one owner, can lower prices when the stages are already imperfectly competitive. The note is the standard origin of what industrial organization now calls double marginalization: when a monopolist upstream sells to a monopolist downstream, each adds its own markup, and the final price is higher than a single integrated monopolist would charge.

The argument underlies the modern economics of vertical mergers and vertical restraints (resale price maintenance, two-part tariffs, franchise fees) and the supply-chain coordination literature in operations research, where a wholesale-price contract between a supplier and a retailer reproduces the same distortion.

A short timeline: Cournot (1838, Chapter IX) analysed complementary monopolists selling inputs to a common product; Spengler (1950) gave the successive-monopoly version and drew the antitrust conclusion; Tirole's textbook (1988, §4.2) made it the canonical example of vertical externalities; Cachon and Lariviere (2005) and the coordination literature studied the same inefficiency in newsvendor supply chains.

Setting

A product passes through three successive stages $A\to B\to C$ before reaching consumers. Production uses fixed proportions: one unit of stage A's product goes into one unit of B's, and one unit of B's into one unit of C's, so all stages handle the same quantity. Each stage has a constant unit variable cost $V_a,V_b,V_c$ (marginal cost equal to average variable cost at every relevant output).

Final demand is a function $D:\mathbb R\to\mathbb R$ : $D(p)$ units of $C$ are bought at price $p$ . A firm with constant unit cost $c$ that sells at price $p$ earns the profit (return above variable outlay)

\pi_c(p)=(p-c)\,D(p),

and $p$ is a profit-maximizing price at cost $c$ when $\pi_c(x)\le\pi_c(p)$ for every $x$ .

Unintegrated chain. Stage A sells to B at a transfer price $P_a$ , B sells to C at $P_b$ . Their per-unit profits are $R_a=P_a-V_a$ and $R_b=P_b-(V_b+P_a)$ ; horizontal integration within each stage lets these be positive "monopolistic surcharges". Stage C's unit cost is $C_c=V_c+P_b$ ; it charges a profit-maximizing price $P_c$ at that cost and sells $Q=D(P_c)$ . The chain's aggregate profit is $R_aQ+R_bQ+R_cQ$ with $R_c=P_c-(V_c+P_b)$ .

Integrated firm. One firm owns all three stages. Its unit cost is $C'_c=V_a+V_b+V_c$ ; it charges a profit-maximizing price $P'_c$ at that cost and sells $Q'=D(P'_c)$ , earning $(P'_c-C'_c)\,Q'$ .

The price elasticity of demand at $p$ is $e(p)=-p\,D'(p)/D(p)$ (positive for a downward-sloping curve) and the marginal revenue is $r(p)=p+D(p)/D'(p)$ . The consumers' surplus gained when the price falls from $P_c$ to $P'_c$ is $\int_{P'_c}^{P_c}D(x)\,dx$ .

Formalization targets

Goal: vertical integration benefits producer and consumer

For every non-increasing demand curve $D$ , all unit costs $V_a,V_b,V_c$ , and all transfer prices with $R_a>0$ , $R_b>0$ , if $P_c$ is profit-maximizing at cost $V_c+P_b$ , $P'_c$ is profit-maximizing at cost $V_a+V_b+V_c$ , $D$ is differentiable at $P_c$ and $Q=D(P_c)>0$ , then

P'_c<P_c,\qquad D(P_c)<D(P'_c),\qquad R_aQ+R_bQ+R_cQ<(P'_c-C'_c)\,Q',

0<\int_{P'_c}^{P_c}D(x)\,dx,\qquad Q\,(P_c-P'_c)\le\int_{P'_c}^{P_c}D(x)\,dx.

The goal fixes no functional form and no numbers; it is the general statement behind the paper's "under all cases conceivable … within the framework here employed".

Milestones

Footnote 6, equilibrium identities. At a profit-maximizing price, $r=c$ , $e=p/(p-r)=p/(p-c)$ , and $p=c\,e/(e-1)$ when $c\ne0$ .
Section III, unitary elasticity. At zero cost, $e=1$ ; at positive cost, $p>c$ and $e>1$ .
Section III, cost raises price. For $c_1<c_2$ , profit-maximizing prices satisfy $D(p_2)\le D(p_1)$ , and $p_1<p_2$ under the goal's regularity hypotheses.
Footnote 6, straight-line demand. For $D(p)=b(a-p)$ : $p^*(c)=(a+c)/2$ , $\Delta r=2\Delta p$ , $e(p^*(c))=(a+c)/(a-c)$ , the elasticity rises relatively more than the price, and the relative rise grows with $c$ .
Figure 1. With $D_c(p)=\tfrac85(140-p)$ and $V_a=V_b=V_c=20$ : $P_c=115$ , $Q=40$ , aggregate profit $2{,}200$ ; $P'_c=100$ , $Q'=64$ , profit $2{,}560$ ; consumers' surplus rises by $780$ .

Significance

The result. The theorem shows that removing an upstream markup can only lower the final price and raise output, so that producers and consumers gain together. This is the economic content of the rule that vertical integration is not anticompetitive as such, and it is the reason modern merger guidelines credit the "elimination of double marginalization" as an efficiency of vertical mergers. Milestone 3, monotonicity of the monopoly price in cost, is the general comparative-statics fact used in tax incidence and cost pass-through.

Formalizing it. The result is classical and proved in every industrial-organization textbook, usually for linear demand. The mission states it for an arbitrary non-increasing demand curve, without concavity, continuity or uniqueness of the profit maximizer, which makes explicit which hypotheses the strict conclusions actually need. Related items on the platform formalize double marginalization in a different model, the newsvendor wholesale-price contract of Cachon and Lariviere, where the supplier-induced order quantity falls short of the integrated one; this mission covers the price-setting, deterministic-demand version.

Difficulty

The weak inequalities ( $P'_c\le P_c$ , $Q\le Q'$ , profit $\le$ ) follow from comparing the two maximization problems (the price comparison also uses $Q>0$ : if $D\equiv 0$ , every price is profit-maximizing). The strict inequalities do not: a demand curve with a kink can have the same profit-maximizing price at two different costs, so integration need not change the price at all. The strict claims therefore need a first-order condition at $P_c$ , and the argument has to combine global optimality (all prices) with local information (a derivative at one point) without assuming the profit function is concave or the maximizer unique. The consumers'-surplus clause requires a lower bound on an integral of a monotone, possibly discontinuous function.

Formalization scope

Prices, costs and quantities are real numbers; maximization is over all prices $p\in\mathbb R$ . Demand is a function $D:\mathbb R\to\mathbb R$ ; the goal assumes only that it is non-increasing (Antitone D).
Profit-maximizing prices are hypotheses (IsProfitMax D c p), never closed forms; the closed form $(a+c)/2$ appears only for straight-line demand.
The transfer prices $P_a,P_b$ are arbitrary data with positive markups; they need not be profit-maximizing for $D_a,D_b$ , which the paper draws only in its figure.
Explicit readings of the paper's prose. "Benefits both producer and consumer" and "will lower the price" become the four strict inequalities of the goal. "Aggregate profit" is the sum over the three stages, $Q[P_c-(V_a+V_b+V_c)]$ , not stage C's profit alone. Consumers' surplus "in the Marshallian sense" is the interval integral of $D$ between the two prices; footnote 5's trapezoid formula is used only for the straight line of Figure 1. Elasticity is a positive number $-pD'(p)/D(p)$ . "Relatively greater increment in the elasticity" is made exact for straight-line demand as $e(p^*(c'))/e(p^*(c))>p^*(c')/p^*(c)$ ; the literal $\Delta e/e>\Delta c/c$ is false for small $c$ . Footnote 6's $e'=(p+\Delta p)/(p-2\Delta p)$ and "approximating $3\Delta p/p$ " are a printed slip; the exact $e(p^*(c))=(a+c)/(a-c)$ is stated instead, and no approximation is formalized. Figure 1's demand line $D_c(p)=\tfrac85(140-p)$ is the line through the three points the text gives.
Added hypotheses. Differentiability of $D$ at $P_c$ and $D(P_c)>0$ , which the paper's marginal-revenue reasoning presupposes. Every statement involving elasticity or marginal revenue carries differentiability and positive demand, because Lean's deriv and division return $0$ on bad input.
Ruled out. Formalizations that hard-code linear demand in the goal, compare the integrated profit with stage C's profit alone, or prove only the weak ( $\le$ ) inequalities do not capture the result.
Sections IV and the policy remarks of Section III (rent evasion, taxes, co-operatives) are not formalized.
Only Mathlib is needed: Fermat's rule (IsLocalMax.hasDerivAt_eq_zero), interval integrals of monotone functions, and real arithmetic. Proofs of the general milestones are reusable for any monopoly-pricing comparative statics.

Selected references

J. J. Spengler, Vertical integration and antitrust policy, Journal of Political Economy 58(4), 1950, 347–352. https://doi.org/10.1086/256964
A. A. Cournot, Recherches sur les principes mathématiques de la théorie des richesses, Hachette, 1838, Chapter IX.
J. Tirole, The Theory of Industrial Organization, MIT Press, 1988, §4.2.
G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

7 thms2 active usersReviewed