Operations Research

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

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.

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

1. 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)$.
2. Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$.
3. 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})$.
4. 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.
5. Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$, then $I(\pi)\ge I(\sigma)$.
6. Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$.
7. 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

Motivation

A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.

Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with $n$ demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.

Setting

A period between two replenishments is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so the period starts in interval $k$ and ends in interval $1$. Demand comes in classes $1,\dots,n$, with class $n$ the most important. At the start of interval $t$ the firm holds stock $z\ge0$ and faces the outstanding demand vector $B=(B^1,\dots,B^n)\ge0$: the backlog $b$ carried in plus the new demand $d_t$, whose law $\mu_t$ on $[0,\infty)^n$ has finite means. Demands of different intervals are independent.

The firm chooses the vector $u$ of demand left unsatisfied, with $0\le u\le B$, so that $w=z-\mathbf 1\cdot(B-u)\ge0$ units remain in stock, where $\mathbf 1\cdot y=\sum_j y^j$. It pays the penalty $p_t\cdot u$ and the holding cost $h_t(w)$. A fraction $a_t\ge0$ of the unsatisfied demand is carried into the next interval: $b_{t-1}=a_tu$, with $a_t=1$ meaning complete backlogging and $a_t=0$ lost sales. At the end of interval $1$ the salvage cost $v_1(z)+v_2(z-\mathbf 1\cdot b)$ is charged. The standing assumptions are:

• (A) $h_t$ is convex and continuous on $[0,\infty)$;
• (B) $v_1$ is convex and continuous on $[0,\infty)$, $v_2$ is convex and continuous on $\mathbb R$, and $D^+v_2$ is bounded below, where $D^+$ is the right derivative;
• (C) $0\le p_t^1\le\cdots\le p_t^n$.

The minimal expected cost $f_t$ of the last $t$ intervals and its expectation $g_t$ satisfy

$$f_t(z,B)=\inf_{\substack{0\le u\le B\\ w=z-\mathbf 1\cdot(B-u)\ge0}}\big[p_t\cdot u+h_t(w)+g_{t-1}(w,a_tu)\big],\qquad g_t(z,b)=\mathbb E\,f_t(z,b+d_t),$$

with $g_0(z,b)=v_1(z)+v_2(z-\mathbf 1\cdot b)$.

For a class $j$, with $\delta_j$ its unit vector, the critical rationing level $\bar z_t^j\in[0,+\infty]$ is $+\infty$ if $\varphi_t^j(w)=p_t^jw+h_t(w)+g_{t-1}(w,a_tw\delta_j)$ is strictly decreasing on $[0,\infty)$, and is the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. With $B^{(j)}=\sum_{i\ge j}B^i$, the rationing level policy leaves unsatisfied

$$u^j=\big(B^{(j)}-z+\bar z_t^j\big)^+\wedge B^j .$$

In words: going down from class $n$, it serves as much of each class as it can without letting the stock fall below that class's critical level.

Formalization targets

Goal: Theorem 1

Suppose $a_i\in\{0,1\}$ for every $i\le t$. Then

1. the rationing level policy attains $f_t(z,B)$ for every $z\ge0$, $B\ge0$;
2. the critical levels are ordered as

$$\bar z_t^1\ge\bar z_t^2\ge\cdots\ge\bar z_t^n;$$

3. for $\varepsilon>0$, the differences $f_t(z,B)-f_t(z+\varepsilon,B+\varepsilon\delta_j)$ and $g_t(z,b)-g_t(z+\varepsilon,b+\varepsilon\delta_j)$ do not depend on $B^1,\dots,B^j$ and $b^1,\dots,b^j$.

Milestones

In attack order:

1. Lemma 1: the infimum of a convex function over one block of variables is convex.
2. Lemma 2: $g_t$ and $f_t$ are convex and continuous on the orthant, and the infimum in (1) is a minimum.
3. The critical levels exist, so they are well defined.
4. Lemma 3: moving $\varepsilon$ of demand from class $i$ to a less important class $j<i$ does not raise $f_t$ or $g_t$.
5. (6): $f_t(z,B)=\min_wf_t(w;z,B)$, where $f_t(w;z,B)$ is the cost of issuing exactly $z-w$ units.
6. Lemma 4: for each $w$, serving the classes in order of importance is optimal.
7. Corollary 1: some optimal $u$ never serves a class before every more important class has been served in full.

A companion item states the paper's remark that with a linear ordering cost $c(y)=c\cdot y$ the optimal order is $y(z)=(y(0)-z)^+$.

Significance

Theorem 1 reduces the $n$-dimensional rationing decision in each interval to $n$ numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on $a_i$ is sharp in the sense the paper shows: for $a_2\in(0,1)$ an example on pp. 165–166 has no optimal policy of this form.

The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.

Difficulty

The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in $w$ (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class-$j$ demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when $0<a_t<1$, so the induction must carry (a), (b) and (c) together and use $a_t\in\{0,1\}$ at every step. A second difficulty is analytic: $f_t$ is an infimum and $g_t$ an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).

Formalization scope

• Representation. Classes are Fin n; the paper's class $j$ is index $j-1$, so class $n$ is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.
• Value functions. $f_t$ is defined by the recursion (1) itself, with a real infimum (sInf), and $g_t$ by a Bochner integral against $\mu_t$. Every statement about $f_t$, $g_t$ is restricted to $z\ge0$ and $B\ge0$ (or $b\ge0$). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.
• Critical levels. The levels live in WithTop ℝ, with $\top=+\infty$. They are specified by the predicate IsCriticalLevel: strictly decreasing for $+\infty$, smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value $0$ when no minimizer exists.
• Standing assumptions. (A)–(C) are imposed for $1\le t\le k$. (B)'s limit condition is read as "$D^+v_2$ is bounded below". $D^+$ is an extended-real right Dini derivative. Assumption (D) on the ordering cost is not used.
• Added hypothesis. Lemma 1 adds the hypothesis that the function is bounded below on every fibre, because a real infimum cannot be $-\infty$.
• Not stated. The paper's remark that Assumption (D) ensures an optimal order $y(z)$ exists for a general continuous $c$ is not formalized. With $n=k=1$, $h_1(w)=w^2$, $c(w)=w-w^2$, $p_1=1$, $v_1=v_2=0$ and demand $1$ with certainty, (D) holds but $c(y)+g_1(y,0)=1-y$ for $y\ge1$, so no minimizer exists.
• Ruled out. Theorem 1 is not proved by assuming Lemma 2, the shape of the optimal vector, or the paper's derivative formulas (8)–(9). Those appear only as milestones or not at all. Part (a) asserts optimality over all feasible $u$, not among rationing level policies.
• Contributions welcome. Proofs of the milestones, general lemmas on convexity of partial infima and on continuity of parametric minima over polytopes, and integrability of functions of linear growth against laws with finite means.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (convexity of partial minima, Theorem 5.7). https://doi.org/10.1515/9781400873173

Motivation

A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector $z(f)$ guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the $n$-discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.

Timeline:

• 1960: Howard, Dynamic Programming and Markov Processes: policy improvement for the discounted and the average-return problems.
• 1962: Blackwell, Discrete Dynamic Programming: existence of stationary policies optimal for all discount factors near one; the expansion $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+o(1)$; nearly optimal (1-optimal) policies characterized by lexicographic maximization of $(x,y)$.
• 1966: Veinott, this paper: the extended policy improvement method that finds a 1-optimal stationary policy in finitely many steps (Theorem 6), and a finite-horizon characterization of the same policies (Theorem 7).
• 1969: Veinott, Discount optimality and sensitive optimality: the full hierarchy of $n$-discount optimal policies and the corresponding nested improvement method.

Setting

There are finitely many states $s$ and a finite set of actions. Choosing action $a$ in state $s$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$. A decision rule $f\in F$ picks an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$ and $Q(f)$ the stochastic matrix with entries $q(s'\mid s,f(s))$. A policy is a sequence $(f_1,f_2,\dots)$ of decision rules, $f^\infty=(f,f,\dots)$ is a stationary policy, and for $0\le\beta<1$

$$V_\beta(\pi)=\sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\,r(f_{n+1})$$

is the vector of expected discounted returns. For vectors, $u\ge v$ is coordinatewise and $u>v$ means $u\ge v$ and $u\ne v$.

Let $Q^*(f)$ be the Cesàro limit of the powers of $Q(f)$. The gain $x(f)$ and the bias $y(f)$ are the unique solutions of

$$[I-Q(f)]x=0,\quad Q^*(f)x=Q^*(f)r(f);\qquad [I-Q(f)]y=r(f)-x(f),\quad Q^*(f)y=0,$$

and $z(f)$ is the unique solution of $[I-Q(f)]z=-y(f)$, $Q^*(f)z=0$. Write $F'$ for the decision rules of maximal gain and $F''\subset F'$ for those of maximal bias within $F'$.

The two improvement sets compare $f$ with a decision rule $g$ through the state-by-state tests

$$\text{(i) } [Q(g)x(f)]_s\ge[x(f)]_s,\qquad \text{(ii) } [r(g)+Q(g)y(f)]_s\ge[x(f)+y(f)]_s .$$

$G(f)$ consists of the $g$ for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and $g(s)=f(s)$ wherever both are equalities. $E(f)$ consists of the $g$ for which (i) and (ii) are equalities at every state. For $g\in E(f)$,

$$\text{(iii) } [-y(f)+Q(g)z(f)]_s\ge[z(f)]_s,$$

and $H(f)$ consists of the $g\in E(f)$ for which (iii) holds everywhere, strictly somewhere, with $g(s)=f(s)$ wherever it is an equality.

Formalization targets

Goal: Theorem 6 (p. 1290)

For every $f\in F$:

1. $G(f)=\varnothing\ \Rightarrow\ f\in F'$;
2. $G(f)\cup H(f)=\varnothing\ \Rightarrow\ f\in F''$;
3. $g\in G(f)\ \Rightarrow\ x(g)>x(f)$, or $x(g)=x(f)$ and $y(g)>y(f)$;
4. $g\in H(f)\ \Rightarrow\ x(g)=x(f)$, and $y(g)>y(f)$, or $y(g)=y(f)$ and $z(g)>z(f)$.

Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises $(x,y,z)$ lexicographically and stops at a decision rule in $F''$.

Milestones

• Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\epsilon(\beta,f)$ with $\epsilon(\beta,f)\to0$ as $\beta\to1^-$, and the unique-solution characterizations of $x(f)$, $y(f)$ (already posed on the platform, referenced).
• Lemma 1 (Blackwell): $g\in E(f)\Rightarrow x(g)=x(f)$, and $y(g)=y(f)$ if moreover $Q^*(g)Q^*(f)=Q^*(g)$ (referenced).
• Theorem 1: for fixed $0\le\beta<1$, exactly one of "$f^\infty$ has no one-step improvement and is $\beta$-optimal" and "some $g$ gives $V_\beta(g,f^\infty)>V_\beta(f^\infty)$ and $V_\beta(g^\infty)>V_\beta(f^\infty)$".
• Theorem 4: $F''$ is the nonempty set of $f$ with $f^\infty$ 1-optimal.
• Theorem 5 and Corollary 1: $G(f)=\varnothing\Rightarrow f\in F'$; $g\in G(f)\Rightarrow V_\beta(g^\infty)>V_\beta(f^\infty)$ for $\beta$ near one, hence the lexicographic increase of $(x,y)$.
• Lemma 4: for $g\in E(f)$, $y(g)=y(f)+w(g)$, where $w(g)$ is the unique solution of $[I-Q(g)]w=0$, $Q^*(g)w=Q^*(g)(-y(f))$.
• (12): $z(f)$ is the unique solution of its system.
• Lemma 5: $G(f)=\varnothing$ and $y(f)\ge y(g)$ for all $g\in E(f)$ imply $f\in F''$.
• Two steps of the proof of Theorem 6: $H(f)=\varnothing\Rightarrow y(g)\le y(f)$ on $E(f)$; and $g\in H(f)\Rightarrow w(g)>w(f)=0$, or $w(g)=w(f)=0$ and $z(g)>z(f)$.

Significance

Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over $F'$, a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set $E(f)$ suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the $n$-discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.

The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and $z$ and the facts about the limit matrix $Q^*$ and the deviation matrix they rest on.

Difficulty

Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set $G(f)$. The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of $g\in E(f)$ cannot be compared with the bias of $f$ by a state-by-state test in the original problem, because $E(f)$ is a product of action sets $E(s,f)$ different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is $-y(f)$ and the role of the gain is played by $w(g)$. A second difficulty is Lemma 5: $E(f)$ may be a proper subset of $F'$ (Example 3 of the paper), so maximizing the bias over $E(f)$ does not obviously maximize it over $F'$. The certificate does not follow from the gain and bias tests at $f$ alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).

Formalization scope

Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's $A_s$ are all equal to it), decision rules St → Act, policies indexed from $0$ (π 0 is $f_1$), real vectors St → ℝ with the pointwise order, and VecGt for the paper's $>$ (not coordinatewise strict). $Q^*(f)$ is the published Cesàro limit $\lim (N+1)^{-1}\sum_{i=0}^N Q(f)^i$, the same limit as Veinott's $N^{-1}\sum_{i=0}^{N-1}$. The gain and bias are the published closed forms $x(f)=Q^*(f)r(f)$ and $y(f)=H(f)r(f)$ with the deviation matrix $H(f)$; the new vectors are closed forms too: $w(g)=Q^*(g)(-y(f))$ and $z(f)=H(f)(-y(f))$, and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set $H(f)$ is HSet, to keep it apart from the deviation matrix Hf.

$G(f)$ and $H(f)$ are defined literally from the paper's inequalities, including the clauses "at least one strict" and "$g(s)=f(s)$ where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a $g$ that only reshuffles ties would count as an improvement); replacing $F''$ or $G(f)$ by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.

The reduction "replace $A_s$ by $E(s,f)$ and $r(g)$ by $-y(f)$" is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities $Q^*Q=QQ^*=Q^*Q^*=Q^*$, $(I-Q)H=I-Q^*$, $Q^*H=0$, would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• A. F. Veinott, Jr., Discount Optimality and Sensitive Optimality, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A convex program is useful in practice only if its optimal value responds reasonably to small changes in the data. Lagrangian and Fenchel duality theory makes this precise: the dual problem attains its optimum and has no duality gap exactly when the primal value function does not fall off infinitely steeply under small perturbations. A constraint qualification is a checkable condition on the data that guarantees this good behaviour; Slater's condition (a strictly feasible point) is the best-known example in finite dimensions.

R. T. Rockafellar's 1967 paper Duality and Stability in Extremum Problems Involving Convex Functions (Pacific J. Math. 21 (1967) 167–187) develops Fenchel-type duality for the problem of minimizing $f(x) - g(Ax)$ in general locally convex spaces. It introduces the notion of a stably set problem, shows that stability is equivalent to strong duality with an attained dual optimum (its Theorem 3), and gives in Theorem 1 a general sufficient condition for stability. Theorem 1 is the infinite-dimensional analogue of Slater's condition and is the form in which the result is usually applied: one exhibits a single point where $f$ is finite and $g$ is finite and continuous.

Timeline. Fenchel (1951) proved the duality theorem for $A = I$ in $\mathbb{R}^n$ under relative-interior conditions. Brøndsted (1964) and Moreau (1966–67) extended conjugate duality to paired locally convex spaces. Rockafellar's 1967 paper (this mission) added the linear map $A$, the perturbation function $h$, the notion of stability, and Theorem 1. The perturbational approach was later systematized in Rockafellar's Conjugate Duality and Optimization (SIAM, 1974).

Setting

Let $E$ and $F$ be real locally convex Hausdorff topological vector spaces and $A : E \to F$ a continuous linear map. Let $f : E \to [-\infty, +\infty]$ and $g : F \to [-\infty, +\infty]$.

• $f$ is convex if its epigraph $\{(x, \mu) \mid x \in E, \mu \in \mathbb{R}, \mu \ge f(x)\}$ is a convex subset of $E \times \mathbb{R}$; it is proper if $f(x) > -\infty$ for all $x$ and $f(x) < +\infty$ for some $x$. $g$ is concave if $-g$ is convex, and proper concave if $g < +\infty$ everywhere and $g > -\infty$ somewhere.
• Throughout, $f$ is lower semicontinuous proper convex and $g$ is upper semicontinuous proper concave. Their effective domains are $C = \{x \mid f(x) < +\infty\}$ and $D = \{y \mid g(y) > -\infty\}$.
• The primal problem is

$$(P) \qquad \text{minimize } f(x) - g(Ax) \text{ over } x \in E,$$

and its perturbations are $(P(z))$: minimize $f(x) - g(Ax - z)$, for $z \in F$. The perturbation function is $h(z) = \inf (P(z)) = \inf_x \{ f(x) - g(Ax - z) \} \in [-\infty, +\infty]$, so $h(0) = \inf (P)$. $(P)$ is consistent if $h(0) < +\infty$.

• When $h(0)$ is finite, the directional derivative is $h'(0; z) = \lim_{\varepsilon \downarrow 0} [h(\varepsilon z) - h(0)]/\varepsilon$.
• $(P)$ is unstably set if $h(0)$ is finite and every neighbourhood of $0$ contains vectors $z$ with $h'(0; z)$ a negative number of arbitrarily large magnitude ($-\infty$ included). $(P)$ is stably set if it is consistent but not unstably set.

Formalization targets

Goal: Theorem 1 (p. 175)

Suppose there exists $x \in E$ such that $f$ is finite at $x$ and $g$ is finite and continuous at $Ax$. Then

$$(P) \text{ is stably set} \quad\text{and}\quad \text{there is a neighbourhood } U \text{ of } 0 \text{ on which } z \mapsto \inf (P(z)) \text{ is continuous}.$$

The neighbourhood $U$ is left unspecified, as in the paper.

Milestones (in the order the proof uses them)

1. (4.4) $\{z \mid h(z) < +\infty\} = \{Ax - y \mid f(x) < +\infty,\ g(y) > -\infty\} = A(C) - D$.
2. (4.5) $A(C)$ meets $\operatorname{int} D$, and $0 \in A(C) - \operatorname{int} D \subseteq \operatorname{int}(A(C) - D)$.
3. Epigraph of $h$ has interior (p. 176): the hypograph $G = \{(y, \mu) \mid g(y) \ge \mu > -\infty\}$ has nonempty interior, $(Ax, \lambda) - G$ lies in the epigraph of $h$ for every $(x, \lambda)$ in the epigraph of $f$, and so the epigraph of $h$ has nonempty interior.
4. Continuity on the interior of the domain (p. 176): $0 \in \operatorname{int}\{h < +\infty\}$ and $h$ is continuous there.
5. (4.6) For a convex $h$ with $h(0)$ finite: $h(z) \ge h(0) + h'(0; z)$ and $h'(0; z) \ge -h'(0; -z)$ for all $z$.

Significance

The result. Combined with the paper's Theorem 3, Theorem 1 yields: if $f$ is finite at some $x$ where $g$ is finite and continuous at $Ax$, then $\inf (P) = \max (P^*)$, with the dual maximum attained. This is the standard sufficient condition for Fenchel–Rockafellar duality in infinite dimensions, used in calculus of variations, optimal control, and the convex analysis of integral functionals. The continuity half of Theorem 1 says that the optimal value depends continuously on translations of the constraint data near the unperturbed problem, a basic sensitivity statement.

Formalizing it. The theorem is proved (1967) and appears in many textbooks, but there is no machine-checked version on this platform. Mathlib contains continuity criteria for real-valued convex functions on open sets of normed or finite-dimensional spaces (ConvexOn.continuousOn_tfae, ConvexOn.continuousOn_interior), but nothing for extended-real-valued convex functions on general topological vector spaces, no perturbation function, and no notion of a stably set problem. A complete development would provide reusable infrastructure: the epigraph-interior continuity criterion for $[-\infty, +\infty]$-valued convex functions and the elementary calculus of one-sided directional derivatives.

Difficulty

The obvious argument says: $g$ is continuous at $Ax$, so $h(z) \le f(x) - g(Ax - z)$ is bounded above near $0$, hence $h$ is continuous at $0$ and its directional derivatives are bounded. Two steps of this fail without care. First, the passage from "bounded above near a point" to "continuous" requires convexity of $h$ (Lemma 2 of the paper, proved in the companion mission) and a continuity criterion valid in an arbitrary topological vector space, with values in $[-\infty, +\infty]$; the normed-space proofs in Mathlib do not apply. Second, $h$ may take the value $-\infty$, and the derivative may be $-\infty$ in some directions; the bookkeeping of extended-real arithmetic (where $(+\infty) + (-\infty)$ is not defined mathematically and is given a junk value in Lean) has to be done honestly. Finally, upper bounds on $h'(0;\cdot)$ must be converted into lower bounds, which is where the second inequality of (4.6) enters; an upper bound alone does not give stability.

Formalization scope

All values are in Lean's EReal. Convexity is convexity of the epigraph with real second coordinate (the paper's definition, p. 170); concavity is convexity of $-g$. Properness is stated as in the paper. The perturbation function is the EReal infimum ⨅ x, f x - g (A x - z); under properness the undefined form $(+\infty) - (+\infty)$ never arises. The directional derivative (4.3) is the lower limit of the difference quotient along $\varepsilon \to 0^+$, which equals the paper's limit whenever it exists (always, for convex $h$ with $h(0)$ finite). "Unstably set" quantifies over all neighbourhoods of $0$ and all real $M$, with $h'(0;z) < -M$ allowing $-\infty$. "Stably set" is $h(0) < +\infty$ together with "not unstably set", so $\inf (P) = -\infty$ is stably set, as the paper says on p. 176. Continuity is with respect to the order topology of EReal, and "continuous at $Ax$" is continuity of $g$ itself at that point, not of its restriction to $D$.

The paper's standing setting (§3) includes dual spaces $E^*, F^*$, the adjoint $A^*$ and the conjugates $f^*, g^*$. Neither Theorem 1 nor its proof uses them, so they are omitted and the theorem is stated for every pair of real locally convex Hausdorff spaces, which includes every paired setting. The lower and upper semicontinuity of $f$ and $g$ are standing hypotheses of the paper and are kept, although the proof does not use them. Inequality (4.6) is stated for an arbitrary convex function finite at $0$, the generality in which the paper invokes it. No statement was repaired.

A definition of "stably set" that already presumed finiteness or continuity of $h$ near $0$, or that tested the derivative only in a fixed set of directions, would make the first conclusion of Theorem 1 trivial; the definition used here is the paper's p. 175 definition verbatim, applied to an arbitrary function $h$. The definitions are local to this mission; the companion missions on Theorem 3 and Theorem 6 of the same paper define the same objects in their own namespaces. Contributions are welcome on the milestones in any order, and in particular on a general continuity criterion for extended-real-valued convex functions on topological vector spaces, which is reusable well beyond this mission.

Selected references

• R. T. Rockafellar, Duality and stability in extremum problems involving convex functions, Pacific J. Math. 21 (1967) 167–187. https://doi.org/10.2140/pjm.1967.21.167
• A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964), no. 2.
• W. Fenchel, Convex Cones, Sets and Functions, lecture notes, Princeton University, 1951.
• J. J. Moreau, Fonctionnelles convexes, Séminaire Leray, Collège de France, 1966–67.
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524