Operations Research

Motivation

Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers $n$ grows while the offered load stays within $O(\sqrt n)$ of $n$. Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).

Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for $k$ customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.

Context:

• Harrison & Zeevi (2004) studied the same multi-class many-server problem.
• Bell & Williams (2001) proved asymptotic optimality of a threshold policy for a two-server system in conventional heavy traffic.
• The present paper is the first to cover the QED regime with general costs and abandonment.

Setting

There are $k\ge1$ customer classes and $n$ identical servers.

Primitives.

• Arrivals. Class-$i$ customers arrive according to a renewal process $A^n_i$ with interarrival times $\check U_i(j)/\lambda^n_i$. Here the $\check U_i(j)$ are i.i.d., positive, of mean one and squared coefficient of variation $C^2_{U,i}$.
• Service. Service times are exponential with rate $\mu^n_i$, represented by Poisson processes $S^n_i$.
• Abandonment. Waiting customers abandon at rate $\theta^n_i\ge0$, represented by Poisson processes $R^n_i$.

State. $X^n_i(t)$ is the number of class-$i$ customers in the system, $\Psi^n_i(t)$ the number in service and $\Phi^n_i=X^n_i-\Psi^n_i$ the number waiting. The dynamics are

$$X^n_i(t)=X^{0,n}_i+A^n_i(t)-R^n_i\Big(\int_0^t\Phi^n_i\Big)-S^n_i\Big(\int_0^t\Psi^n_i\Big),\qquad \Psi^n,\Phi^n\in\mathbb Z^k_+,\quad \textstyle\sum_i\Psi^n_i\le n .$$

Policies.

• A scheduling control policy (SCP) is the process $\Psi^n$.
• It is admissible if it does not anticipate the future beyond the time of the next arrival: past information is independent of future primitive increments.
• It is work-conserving if no server idles while customers wait: $(\mathbb 1\cdot X^n-n)^+=\mathbb 1\cdot\Phi^n$.

Scaling and cost. In the QED scaling $n^{-1}\lambda^n_i\to\lambda_i$ with $\sum_i\lambda_i/\mu_i=1$. With $\rho_i=\lambda_i/\mu_i$ the centred processes are $\hat X^n=n^{-1/2}(X^n-\rho n)$, $\hat\Phi^n=n^{-1/2}\Phi^n$ and $\hat\Psi^n=n^{-1/2}(\Psi^n-\rho n)$. The cost is

$$C^n=E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n(t),\hat\Psi^n(t))\,dt .$$

The limiting control problem. It controls

$$X(t)=x+rW(t)+\int_0^t b(X(s),u(s))\,ds,\qquad b(x,u)=\ell+(\mu-\theta)(\mathbb 1\cdot x)^+u-\mu x,$$

where the control $u$ takes values in the simplex $\mathbb S^k$ and $W$ is a $k$-dimensional Brownian motion. The data are $r_i=(\lambda_iC^2_{U,i}+\lambda_i)^{1/2}$ and $\ell_i=\hat\lambda_i-\rho_i\hat\mu_i$. Its value $V(x)$ is the infimum of $E\int_0^\infty e^{-\gamma t}L(X,u)\,dt$, with $L(x,u)=\tilde L((\mathbb 1\cdot x)^+u,x-(\mathbb 1\cdot x)^+u)$.

HJB equation and the proposed policy. The HJB equation is $\tfrac12\sum_ir_i^2\partial_{ii}f+H(x,Df)-\gamma f=0$ with $H(x,p)=\inf_{u\in\mathbb S^k}[b(x,u)\cdot p+L(x,u)]$. Let $h$ be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to $\Theta[(\mathbb 1\cdot X^n-n)^+h(\hat X^n)]$, an integer rounding, and falls back to a static priority rule when that is infeasible.

Formalization targets

Goal: Theorem 2(i)

For a $C^2_{\mathrm{pol}}$ solution $f$ of the HJB equation, a measurable minimizer selection $h$, and initial states with $\hat X^{0,n}\to x$:

$$\lim_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^{n,*}_t,\hat\Psi^{n,*}_t)\,dt\;\le\;\liminf_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n_t,\hat\Psi^n_t)\,dt$$

This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.

Milestones

The milestones follow the proof:

• on the diffusion side, Proposition 2 (well-posedness), Proposition 4 (stability and moment bounds), Proposition 5(i)–(ii) (growth and continuity of $V$) and Theorem 3 ($V$ is the unique $C^2_{\mathrm{pol}}$ HJB solution, and an optimal Markov policy exists);
• on the queueing side, Proposition 1 (feedback rules give admissible SCPs), Lemmas 2–3 (moment bounds), Lemma 4(i)–(ii) (FCLT for the primitives and the fluid limit $(\bar\Psi^n,\bar\Phi^n)\Rightarrow(\rho,0)$), and Theorem 4(i)–(ii): $\liminf\ge V(x)$ always, and $\limsup\le V(x)$ under condition (49).

Significance

The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given $h$, and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with $V(x)$.

Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:

• a counting-process model of the queue;
• a careful definition of non-anticipation;
• a pathwise controlled SDE;
• classical solvability of a semilinear elliptic HJB equation on $\mathbb R^k$;
• a weak-convergence argument in Skorokhod space.

Each of these is reusable well beyond this paper.

Difficulty

The obvious argument would show that $\hat X^n$ converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:

• the comparison class contains arbitrary non-Markov, history-dependent policies, so the queue does not converge to a single controlled diffusion;
• the optimal selector $h$ is in general discontinuous (for linear costs it is), so the proposed policy is not a continuous function of the state.

The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:

• uniform moment bounds;
• tightness of the integral processes;
• the convergence of stochastic integrals of Kurtz and Protter;
• and, for the proposed policy, the fact that the rounding $\Theta$ and the priority fallback perturb the minimizer by $O(n^{-1/2})$.

Existence of a classical HJB solution on all of $\mathbb R^k$, with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.

Formalization scope

The Lean development commits to the following conventions.

• Indexing and norms. Classes are Fin k with $k\ge1$; paper class $i$ is index $i-1$, so "class $k$" (highest priority, rounding remainder of $\Theta$) is the last index. Vectors are Fin k → ℝ and $\|\cdot\|$ is the paper's $\ell^1$ norm; the paper's $|\cdot|$ on vectors is read the same way.
• Probability space and paths. All systems share one complete probability space. Time is real and every condition is for $t\ge0$. The paper's "without loss" path regularity (finite arrival counts, Poisson paths $\mathbb Z_+$-valued, nondecreasing and càdlàg) holds for every $\omega$.
• Poisson processes are defined by independent Poisson increments; rate $0$ gives the zero process.
• Policies. A policy is a pair of real processes $(\Psi^n,X^n)$ with integer values. Admissibility is Definition 2 verbatim, with the future $\sigma$-field built from the next arrival time $\tau^n_i(t)$. Work conservation is (18).
• Costs and value are lower Lebesgue integrals in $[0,\infty]$, and $\lim$/$\liminf$ are taken there. The integrands are nonnegative under work conservation.
• Admissible systems range over sample spaces Ω : Type (universe 0). "Complete filtered probability space" means $P$ complete with all null sets in $\mathcal F_0$. Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the $(\mathcal F_t)$-Brownian property stated explicitly. $V$ is the infimum over systems and their controlled processes.
• Discount rate. $\gamma>0$ is a hypothesis; the paper leaves it implicit.
• Initial states are integer vectors $X^{0,n}\in\mathbb Z^k_+$ with $n^{-1/2}(X^{0,n}-\rho n)\to x$. The literal "$\hat X^{0,n}\in n^{-1/2}\mathbb Z^k$" would require $\rho_in\in\mathbb Z$. Assumption 1(ii) is not imposed: each policy chooses its own initial split.
• Lemma 3 is stated for all $n$ beyond a threshold that depends on the sequence, with constants $c,\bar m$ chosen before $x$ and the sequence. The printed all-$n$ bound with $c$ independent of $x$ fails when the early terms $\hat X^{0,n}$ are large.
• Weak convergence to a continuous limit uses the coupling form CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.

The goal hypothesizes $f$ and $h$ with the pointwise identity $b(x,h(x))\cdot Df(x)+L(x,h(x))=H(x,Df(x))$ for all $x$. An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where $\hat X^n$ lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing $k$, dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.

Not formalized:

• Lemma 4(iii) (tightness);
• Lemma 5 (Kurtz–Protter, which needs semimartingale theory absent from Mathlib);
• Lemma 6 (convergence of Stieltjes integrals at limit points);
• Proposition 5(iii);
• the nonpreemptive results, Theorem 2(ii)–(iii).

Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.

Selected references

• R. Atar, A. Mandelbaum, M. I. Reiman, Scheduling a multi class queue with many exponential servers: asymptotic optimality in heavy traffic, Ann. Appl. Probab. 14(3), 2004. https://arxiv.org/abs/math/0407058
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manuf. Serv. Oper. Manag. 5(2), 2003. https://doi.org/10.1287/msom.5.2.79.16071
• J. M. Harrison, A. Zeevi, Dynamic scheduling of a multiclass queue in the Halfin–Whitt heavy traffic regime, Oper. Res. 52(2), 2004. https://doi.org/10.1287/opre.1040.0109
• S. L. Bell, R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11(3), 2001. https://doi.org/10.1214/aoap/1015345343
• T. G. Kurtz, P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19(3), 1991. https://doi.org/10.1214/aop/1176990334

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

• 1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
• 1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
• 1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$, an order cost rate $c^d$, a shipment cost rate $c^r$, a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$, shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$, and $u^{(i)}$ denotes the sum of $i$ copies.

The state is $(\hat y, v^d, x^r)$:

• $\hat y = (y^1, \dots, y^L)$ lists the outstanding orders, $y^i$ placed $i$ periods ago;
• $v^d$ is the depot's echelon inventory (its own stock plus $x^r$);
• $x^r$ is the outlet's stock plus shipments in transit.

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$. With demand $u$, the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$. The one-period cost is

$$c^d(y) + h^d(v^d + y^L) + c^r z + R(x^r + z),$$

where $c^d(y) = K + c^d y$ for $y > 0$, $c^d(0) = 0$, and

$$R(x) = \alpha^l\{-h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r)E[x - u^{(l+1)}]^+\}.$$

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$.

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$. The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$, action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$. The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$: up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$. For every state with $\hat y \ge 0$ and $x^r \le v^d$, and every admissible policy $\pi$,

$$B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).$$

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$, $g_n^r$, $\hat g_n^d$, $g_n^d$ for the $n$-period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$, and of the depot with penalty $P$.

• Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$.
• Property (e): $g_n^r \to g^r = B^{r\alpha}$.
• §2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$.
• Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$.
• Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
• Lemma 3: $\hat g_n \to g^d + g^r$.
• Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$, built from the outlet's optimal costs $g_{n-1}^r$, and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$, and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$. Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$, and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

• Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$, whose index $k$ is the paper's $y^{k+1}$. For $L = 0$ the current order arrives at once.
• Policies and cost. Time runs forward with weight $\alpha^k$; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
• Finite-horizon programs. These are real infima over the feasible actions.
• Hypotheses. Statements quantify over the physical states $\hat y \ge 0$, $x^r \le v^d$. The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$, demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$; that is the paper's definition of $\pi_\alpha^*$, and its existence is Iglehart's.
• Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
• Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$, $n \ge 2$, and eventually, respectively. The moderation notes give the counterexample at $n = 1$. Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
• Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$, value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

• A. Federgruen, P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark, H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.

Timeline.

• Clark and Scarf (Management Science 1960) showed that the finite-horizon, discounted problem of a serial system decomposes: an optimal policy is obtained by solving the most downstream location alone, charging its shortfalls to the upstream location through an induced penalty cost, and then solving the upstream location as a single-location problem with that penalty.
• Iglehart (Management Science 1963, and a 1963 chapter in Multistage Inventory Models and Techniques) established the infinite-horizon theory of the single-location problem with a fixed order cost: optimality of stationary $(s,S)$ policies under discounted and average costs, and the convergence of value iteration.
• Federgruen and Zipkin (Operations Research 1984) carried the decomposition to the infinite horizon for a depot and one retail outlet, under discounted costs (Theorem 1) and under the average-cost criterion (Theorem 2). This mission is about the average-cost case, §3 of that paper.

Setting

Time is divided into periods. A depot orders from an outside supplier with lead time $L \ge 0$ and supplies a retail outlet with shipment lead time $l \ge 0$. The demand $u$ in each period is a nonnegative random variable with law $\nu$ and finite mean $\mu$; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.

The state is $(\tilde y, v^d, x^r)$:

• $\tilde y = (y^1,\dots,y^L)$ lists the orders placed $1,\dots,L$ periods ago;
• $v^d$ is the depot's echelon inventory, its own stock plus the outlet's inventory position;
• $x^r$ is the outlet's inventory position, its stock plus shipments in transit.

In each period the decision is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$, where $y^L$ is the order arriving now. The state then moves to $((y, y^1,\dots,y^{L-1}),\, v^d + y^L - u,\, x^r + z - u)$.

Costs are a fixed order cost $K$, proportional order and shipment rates $c^d$ and $c^r$, a holding rate $h^d$ on system inventory, an extra holding rate $h^r$ at the outlet and a backorder penalty rate $p^r$. After the paper's accounting transformation, the one-period cost is

$$c^d(y) + D(v^d + y^L) + c^r z + R(x^r + z),$$

with $c^d(y) = K + c^d y$ for $y > 0$ and $c^d(0) = 0$, $D(v) = h^d v$, and, at $\alpha = 1$,

$$R(x) = -h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r) E[x - u^{(l+1)}]^+ ,$$

where $u^{(l+1)}$ is the demand over $l + 1$ periods. The critical number $x^{r*}$ is a minimizer of $R$. The stationary induced penalty is $P(x) = R(x) - R(x^{r*})$ for $x < x^{r*}$ and $0$ otherwise.

For a policy $\pi$ and initial state $s$, $B_n(s \mid \pi)$ is the expected cost of the first $n$ periods and $B(s \mid \pi) = \limsup_n B_n(s \mid \pi)/n$ is the average cost. Problem IH asks for a policy minimizing $B(s\mid\cdot)$ from every state. The depot problem IH$^d$ has states $(\tilde y, v^d)$, orders $y \ge 0$ and one-period cost $c^d(y) + D(v^d + y^L) + P(v^d + y^L)$. Its minimal average cost is $a^d$. The outlet problem has states $x^r$, shipments $z \ge 0$ and one-period cost $c^r z + R(x^r + z)$. The policy $\pi^*$ orders by an optimal stationary policy of IH$^d$ and ships $z = \max(0, \min(x^{r*}, v^d + y^L) - x^r)$: up to the critical number if the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 2 (p. 828)

With $\alpha = 1$ and $c^d = c^r = 0$, the policy $\pi^*$ is measurable and feasible from every physical state, and for every such state $s$ and every measurable feasible policy $\pi$,

$$B(s \mid \pi^*) \le B(s \mid \pi).$$

Milestones

• Property (f) (p. 824): $g^r_n(x)/n \to B^r(x) = c^r\mu + R(x^{r*})$ for the outlet program $g^r_n$.
• Eq. (4) (p. 823), for $0 \le \alpha \le 1$: $\hat g_n(\tilde y, v^d, x^r) = \hat g^d_n(\tilde y, v^d) + g^r_n(x^r)$.
• §3 claims (p. 828): with $c^r = 0$, $x^{r*}$ is the critical number of every period, $g^r_n(x) = nR(x^{r*})$ for $x \le x^{r*}$, $\hat P_n = P$, $\hat g^d_n = g^d_n$ and $\hat g_n = g_n$.
• §3 display (p. 828): $\hat g_n(\tilde y, v^d, x^r)/n \to a = a^d + R(x^{r*})$.
• Lemma 5 (p. 828): $B(s \mid \pi^*) = a$.
• Proof of Theorem 2 (p. 828): $\hat g_n(s) \le B_n(s \mid \pi)$ for every measurable feasible $\pi$.

Significance

The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location $(s,S)$-type problem for the depot with a known convex penalty $P$, and a myopic critical-number rule for the outlet. The optimal system cost is the sum $a^d + a^r$ of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":

• the class of measurable history-dependent policies;
• the expected costs of policies with unbounded one-period costs;
• the passage from history-dependent to Markov policies;
• the transient of $\pi^*$ when the outlet starts above its critical number.

Difficulty

The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that $\pi^*$ attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions $K$-convex rather than convex.

The paper's route avoids that equation but needs three separate facts:

• value iteration for the whole system, divided by $n$, converges to $a^d + a^r$, which rests on Iglehart's convergence for the depot and on the stationarity of the penalties when $c^r = 0$;
• the finite-horizon value bounds the cost of every history-dependent policy, not only of Markov ones;
• $\pi^*$ achieves $a$ from every state, including states with $x^r > x^{r*}$, where it does not ship at all until demand has brought the outlet below its critical number.

Formalization scope

• Representation. A state is a triple in $(\mathrm{Fin}\,L \to \mathbb R) \times \mathbb R \times \mathbb R$. For $L = 0$ the order placed now arrives at once. Time runs forward in Lean; the paper numbers periods backward. Finite-horizon value functions keep the paper's index $n$ (periods remaining). Each "min" of programs (1), (2), (3), (5) is a real infimum over the constraint set.
• Policies and costs. Policies are deterministic, history-dependent and measurable, and they must be feasible along every demand realization. $B_n$ is an extended real (expected positive part minus expected negative part of each period's cost). $B$ is a $\limsup$ in the extended reals, and the optimal average costs are infima in the extended reals.
• Standing assumptions (p. 821):
  • $K, h^d, h^r, p^r > 0$;
  • demands i.i.d., nonnegative, without atoms ("for convenience we shall assume $u$ is continuous") and with finite mean.
• Added hypotheses.
  • States are restricted to the physical ones, $\tilde y \ge 0$ and $x^r \le v^d$.
  • $c^d = c^r = 0$. The paper reduces to this case "without loss of generality", on the grounds that average proportional costs equal $c^d\mu$ and $c^r\mu$ "under all interesting policies" (p. 827). That class is never specified, and the proofs are written for $c^d = c^r = 0$. The general-cost version is the paper's informal reduction and is not part of the goal.
  • Eq. (4) is stated for $0 \le \alpha \le 1$ with $K, h^d, h^r, p^r > 0$ and $c^d, c^r \ge 0$ (so that it covers §3's case $c^d = c^r = 0$), and with the relation $\alpha^l p^r \ge (1 - \alpha^l)h^d$, which the paper names on p. 827; it holds automatically at $\alpha = 1$.
• Ruling out trivial readings.
  • $\pi^*$ is built from a depot rule $\sigma^d$ assumed optimal for IH$^d$ from every depot state. Its existence is Iglehart's theorem, cited and not formalized; no $(s,S)$ form is required.
  • The goal quantifies over all measurable feasible policies, and $\pi^*$'s own feasibility is a conclusion, so a vacuous policy class cannot satisfy it.
  • A sorry-free check in the workspace exhibits an instance (exponential demand) meeting every standing hypothesis other than the optimality of $\sigma^d$, including the existence of $x^{r*}$.
• Reusable infrastructure. The definitions of history-dependent policies and of extended-real expected and average costs for controlled processes driven by i.i.d. real noise are generic, and could be reused for other inventory and queueing models. Contributions are welcome on any milestone, and especially on a formal version of the Markov reduction (Dynkin–Yushkevich III.1) for this setting and on Iglehart's convergence of $g^d_n/n$.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. L. Iglehart, Dynamic Programming and Stationary Analyses of Inventory Problems, Chapter 1 in H. Scarf, D. Gilford and M. Shelly (eds.), Multistage Inventory Models and Techniques, Stanford University Press, 1963.
• E. B. Dynkin and A. A. Yushkevich, Controlled Markov Processes, Springer, 1979.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

Motivation

Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.

Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).

Timeline:

• 1965: Blackwell, discounted dynamic programming on Borel spaces with Borel-measurable data, case (D).
• 1966: Strauch, negative dynamic programming, case (N), with Borel-measurable data.
• 1978: Bertsekas and Shreve, Chapter 9: lower semianalytic costs and universally measurable policies, in all three cases (P), (N), (D).
• 1979: Shreve and Bertsekas, the journal account of universally measurable policies.

Setting

An infinite horizon stochastic optimal control model (SM) is an eight-tuple $(S, C, U, W, p, f, \alpha, g)$. The state space $S$, the control space $C$ and the disturbance space $W$ are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint $U$ assigns to each state $x$ a nonempty set $U(x) \subseteq C$, and the set $\Gamma = \{(x,u) \mid u \in U(x)\}$ is analytic. The disturbance kernel $p(dw \mid x, u)$ is a Borel stochastic kernel and the system function $f : SCW \to S$ is Borel. The discount factor is $\alpha > 0$, and the one-stage cost $g : \Gamma \to [-\infty, \infty]$ is lower semianalytic: each sublevel set $\{g < c\}$ is analytic. The state moves by $x_{k+1} = f(x_k, u_k, w_k)$, with transition kernel $t(B \mid x, u) = p(\{w \mid f(x,u,w) \in B\} \mid x, u)$.

A policy $\pi = (\mu_0, \mu_1, \dots)$ chooses $u_k$ at random from a universally measurable stochastic kernel $\mu_k(du_k \mid x_0, u_0, \dots, x_k)$ concentrated on $U(x_k)$; $\Pi'$ is the set of all policies. A policy is Markov if each $\mu_k$ depends only on $x_k$, and it is stationary if, moreover, $\mu_k = \mu$ for all $k$. Writing $q_k(\pi, p_x)$ for the law of $(x_k, u_k)$ started from $x_0 = x$, the cost of $\pi$ and the optimal cost are

$$J_\pi(x) = \sum_{k=0}^\infty \alpha^k \int g\, dq_k(\pi, p_x), \qquad J^*(x) = \inf_{\pi \in \Pi'} J_\pi(x).$$

For $J : S \to [-\infty, \infty]$, the dynamic programming operators are

$$T(J)(x) = \inf_{u \in U(x)} \Big\{ g(x,u) + \alpha \int_S J(x')\, t(dx' \mid x, u) \Big\}, \qquad T_\mu(J)(x) = \int_C \Big[ g(x,u) + \alpha \int_S J\, dt \Big] \mu(du \mid x).$$

The three cases are (P) $g \ge 0$ on $\Gamma$; (N) $g \le 0$ on $\Gamma$; (D) $\alpha < 1$ and $|g| \le b$ on $\Gamma$ for some real $b$.

Formalization targets

Goal: the optimality equation (Proposition 9.8, Eq. (22))

Under each of (P), (N) and (D),

$$J^* = T(J^*).$$

Milestones

• $J^*$ is lower semianalytic (Corollary 9.4.1).
• For a stationary policy, $J_\mu = T_\mu(J_\mu)$ (Proposition 9.9).
• Optimality tests for stationary policies: under (P) or (D), $(\mu, \mu, \dots)$ is optimal iff $J^* = T_\mu(J^*)$ (Proposition 9.12); under (N) or (D), iff $J_\mu = T(J_\mu)$ (Proposition 9.13).
• Under (N) or (D), value iteration from $0$ converges to $J^*$, and under (D) it converges uniformly from every bounded lower semianalytic start (Proposition 9.14).

Further statements of the mission

• Markov policies suffice: at each state some Markov policy matches any policy's cost (Proposition 9.1), so $J^* = \inf_{\pi \in \Pi} J_\pi$ (Corollary 9.1.1).
• Partial converses of the optimality equation: $J \ge T(J)$, $J \ge 0$ gives $J \ge J^*$ under (P); $J \le T(J)$, $J \le 0$ gives $J \le J^*$ under (N); a bounded solution of $J = T(J)$ equals $J^*$ under (D) (Proposition 9.10). The analogous statements for $T_\mu$ and $J_\mu$ (Proposition 9.11).

Significance

The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for $\varepsilon$-optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.

All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.

Difficulty

Under (D), $T$ is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals $J^*$ requires knowing that $J^*$ belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: $\lim_k J_k(0) = 0$ while $J^*(0) = \infty$). Even when each $J_k$ is Borel, $J^*$ may fail to be (Example 2). So $J^* = T(J^*)$ cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines $T$.

The book's route lifts (SM) to a deterministic model on the space of probability measures $P(S)$, where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.

Formalization scope

The draft fixes the following conventions.

• Spaces. Borel spaces are topological spaces homeomorphic to Borel subsets of complete separable metric spaces, carrying their Borel $\sigma$-algebras. Analytic sets are Mathlib's AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.
• Extended reals. Values lie in EReal. The book's convention $\infty - \infty = -\infty + \infty = \infty$ is implemented explicitly, because Mathlib's EReal sets $\bot + \top = \bot$. The integral of an extended-real function is $\int f^+ - \int f^-$ with the same convention.
• Policies. These are sequences of universally measurable stochastic kernels on the history spaces $S_0C_0 \cdots S_k$, charging $U(x_k)$ with mass one. The laws of $(x_0, u_0, \dots, x_k, u_k)$ are built recursively from the kernels.
• Costs. $J_\pi$ is the series $\sum_k \alpha^k \int g\, dq_k$, computed as the difference of the series of positive and negative parts. Under each of (P), (N), (D) it coincides with the integral of the total discounted cost. $J^*$ is the infimum over all policies.
• Case labels. Each statement carries the case labels the book attaches to it, as hypotheses on the model.
• Scope. Only the (SM) statements are formalized. The deterministic model (DM) on $P(S)$ is the book's proof device and enters no statement.

The goal admits a trivializing formalization that this draft rules out. $J^*$ is not defined as a fixed point of $T$, nor as the limit of $T^k(0)$; it is the infimum of the costs of all policies, which under (P) can differ from that limit.

A complete development needs universally measurable kernels and their compositions on product spaces, measurability of $x \mapsto \int f(x, y)\, q(dy \mid x)$ for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996. Chapter 9. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

The maximum flow problem asks how much of a commodity can be shipped from a source to a sink through a network whose arcs have limited capacities. L. R. Ford, Jr. and D. R. Fulkerson's 1956 paper Maximal Flow Through a Network proved the minimal cut theorem: the largest flow value equals the smallest total capacity of a set of arcs that separates source from sink. That theorem is formalized in the companion mission Maximal Flow Through a Network I.

The second section of the same paper treats a special class of networks, those that remain planar after an arc from source to sink is added. For these networks the paper shows that one particular source–sink chain crosses every minimal separating set exactly once. This structural fact turns the minimal cut theorem into a simple computing procedure: repeatedly push as much flow as possible along such a chain and delete the arcs it saturates. The paper notes that G. Dantzig had conjectured, before the minimal cut theorem was proved, that this procedure yields a maximal flow on planar networks. The same "uppermost path" idea underlies later algorithms for maximum flow in planar graphs with source and sink on a common face (Itai and Shiloach, 1979).

The statement is short and purely combinatorial in its conclusion, but its hypothesis is topological. This mission isolates that theorem.

Setting

A network $N$ has a finite set $V$ of vertices and a finite set $E$ of arcs. Each arc $e$ joins two distinct end vertices, written $\mathrm{tail}(e)$ and $\mathrm{head}(e)$; arcs carry no direction, and two arcs may join the same pair of vertices. Two distinct vertices are distinguished, the source $a$ and the sink $b$, and each arc carries a positive capacity (capacities play no role in the target below).

A chain joining $u$ and $w$ is a set $C$ of distinct arcs that can be arranged as $\alpha_1(v_0v_1), \alpha_2(v_1v_2), \dots, \alpha_k(v_{k-1}v_k)$ with $v_0 = u$, $v_k = w$, and the vertices $v_0, \dots, v_k$ pairwise distinct; each arc may be traversed in either direction. The empty set is the null chain from $u$ to $u$.

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$. A disconnecting set none of whose proper subsets is disconnecting is a cut.

The network is ab-planar if the graph of $N$, together with one additional arc joining $a$ and $b$, can be drawn in the plane without crossings: vertices go to distinct points of $\mathbb R^2$; each arc, including the added arc $ab$, goes to an injective continuous path between the points of its end vertices; no arc passes through a vertex other than its ends; and two distinct arcs meet only at endpoints of both. In Lean the drawing is the structure ABPlaneDrawing N, and $N$ is ab-planar when Nonempty (ABPlaneDrawing N). The section's standing assumption is that no arc of $N$ already joins $a$ and $b$.

Formalization targets

Goal: Theorem 2 (p. 403)

If $N$ is ab-planar, no arc of $N$ joins $a$ and $b$, and some chain joins $a$ and $b$, then

$$\exists\, T \text{ a chain joining } a \text{ and } b \ \text{ such that }\ |T \cap D| = 1 \ \text{ for every cut } D \text{ of } N.$$

This is FordFulkerson56.Planar.ab_planar_exists_chain_meeting_each_cut_once. "Precisely once" is exact cardinality one, neither "at least once" (true of every chain) nor "at most once".

Milestone: a chain meeting a cut in one prescribed arc (proof of Theorem 2, p. 403)

For every network $N$, every cut $D$ and every arc $\alpha \in D$, there is a chain $C$ joining $a$ and $b$ with $C \cap D = \{\alpha\}$. No planarity is involved; the statement is what the minimality of a cut provides to the proof.

Further item: the Fig. 2 example (p. 403)

In the "gas, water, electricity" graph $K_{3,3}$ with the arc $ab$ removed, every chain joining $a$ and $b$ meets some cut in three arcs. This network is not ab-planar, so the example shows that the planarity hypothesis of Theorem 2 cannot be dropped.

Significance

Theorem 2 and the minimal cut theorem together give the paper's procedure for planar networks: if $T$ meets every cut once, then imposing a flow $k$ on $T$ lowers the value of every cut by exactly $k$, so the minimal cut value, and hence the maximal flow value, drops by $k$. Saturated arcs can then be deleted and the step repeated. Without the "exactly once" property the reduction could overshoot the cut structure, and the greedy step would not be justified. The theorem is also one of the earliest instances of the link between planarity and cut structure that later underlies planar duality arguments for minimum cuts.

The result has been known since 1956 and is not open. No machine-checked version is recorded on the platform, and Mathlib, at the pinned revision, has neither planar graphs nor the Jordan curve theorem. A formal proof would be the first formalized statement about source–sink planar networks in this library, and the counterexample item records, as a checkable fact, that the hypothesis is necessary.

Difficulty

The conclusion is combinatorial while the hypothesis is a drawing in $\mathbb R^2$. The paper's proof normalises the drawing (the added arc $ab$ on the outer boundary, the graph in a vertical strip with $a$ on the left line and $b$ on the right), selects the "top-most" chain from $a$ to $b$, and argues that a chain meeting a cut below the top-most chain must cross another such chain. Each of these steps rests on plane topology: the existence of the outer region, the meaning of "top-most", and the fact that two chains with interleaved endpoints on a boundary must intersect, which is a form of the Jordan curve theorem.

The naive purely combinatorial route fails: the analogous statement for arbitrary networks is false (Fig. 2), so any argument has to use the drawing somewhere. Replacing the drawing by a combinatorial embedding (rotation systems, faces) is possible but then requires proving that the two notions agree, which is again Jordan-curve territory.

Formalization scope

Conventions committed to in the Lean statements:

• Vertices and arcs are finite types V, E with decidable equality. Arcs are undirected, may be parallel, and have two distinct end vertices. Source and sink are distinct, capacities are positive (structure Network).
• A chain is a Finset E that is the arc set of some arrangement as a simple path (IsChainWalk, IsChain); the null chain is allowed.
• IsDisconnecting and IsCut quantify over all chains joining source and sink; a cut is a disconnecting set no proper subset of which is disconnecting.
• ab-planarity is a plane drawing of the graph with the extra arc indexed by none : Option E, with injective Paths in ℝ × ℝ as arcs.

Hypotheses of the goal: hno_ab, the standing assumption of §2 (no arc joins $a$ and $b$, p. 403); hconn, that some chain joins $a$ and $b$. The second is not stated in the paper; its proof starts from "the chain joining a and b which is top-most", which presupposes one, and without it the statement is false (if $a$ and $b$ are disconnected, the empty set is a cut and no chain exists).

The drawing structure is satisfiable (a three-vertex path network has an explicit drawing), so the planarity hypothesis is not vacuous; and it covers the added arc $ab$ and all crossings, so $K_{3,3}$ minus $ab$ is not ab-planar and the goal is not refuted by the paper's own example. A formalization that dropped the arc $ab$ from the drawing, or quantified over disconnecting sets instead of cuts, would state a false theorem and is ruled out.

A complete development needs basic plane topology for paths in $\mathbb R^2$ (a Jordan-curve-type separation lemma for simple closed curves, or an equivalent statement about crossing paths in a strip), together with combinatorial lemmas about chains (concatenation and shortcutting of chains at a common vertex). The topological lemmas are reusable well beyond this mission. Proofs through a combinatorial embedding are welcome, provided the equivalence with ABPlaneDrawing is proved.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• A. Itai and Y. Shiloach, Maximum flow in planar networks, SIAM Journal on Computing 8 (1979), 135–150. https://doi.org/10.1137/0208012
• H. Whitney, Planar graphs, Fundamenta Mathematicae 21 (1933), 73–84. https://doi.org/10.4064/fm-21-1-73-84

Motivation

Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow $\dot x=-\nabla f(x)$ for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic $f$ this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value $+\infty$, by replacing $\|\nabla f\|$ with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower-$C^2$ functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).

Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to $C^1$ functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.

Setting

Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$. The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\neq x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge0$. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $x_k\to x$ and $f(x_k)\to f(x)$. The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|: x^*\in\partial f(x)\}$, equal to $+\infty$ when $\partial f(x)=\emptyset$, and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points.

The standing assumptions of Section 4 are:

• $(\mathcal H1)$ $f$ is either lower semicontinuous and convex, or lower-$C^2$ with $\operatorname{dom} f=\mathbb R^n$. Lower-$C^2$ means that near each point $f=\max_{s\in S}F(\cdot,s)$ for a compact space $S$ and a jointly continuous $F$ with jointly continuous first and second $x$-derivatives.
• $(\mathcal H2)$ $f$ is somewhere finite and bounded from below.
• $(\mathcal H3)$ $f$ is subanalytic: its graph is locally the projection of a bounded set defined by finitely many real-analytic equalities and strict inequalities.

A trajectory of the subgradient system $(\mathcal G)$ is an absolutely continuous curve $x:[0,T)\to\mathbb R^n$, $T\in(0,+\infty]$, with $\dot x(t)+\partial f(x(t))\ni0$ for almost every $t$ and $\partial f(x(t))\neq\emptyset$ for every $t$. It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around $a$ with exponent $\theta$ if $|f-f(a)|^\theta/m_f$ is bounded near $a$, with $0^0=1$ and $\infty/\infty=0/0=0$. A Łojasiewicz exponent at $a\in\operatorname{dom} f$ is any such $\theta\in[0,1)$.

Formalization targets

Goal: Theorem 4.7

Under $(\mathcal H1)$–$(\mathcal H3)$, every bounded maximal trajectory $x$ is defined on $[0,+\infty)$ and converges to a critical point $a$. For every Łojasiewicz exponent $\theta$ at $a$ there are $k,k'>0$ and $t_0\ge0$ such that for $t\ge t_0$

$$\|x(t)-a\|\le \begin{cases} k\,(t+1)^{-\frac{1-\theta}{2\theta-1}}, & \theta\in(\tfrac12,1),\\[2pt] k\,e^{-k't}, & \theta=\tfrac12,\end{cases}$$

and for $\theta\in[0,\tfrac12)$, $x(t)=a$ for all large $t$. The constants are existential, so the goal survives any later sharpening of them.

Milestones

1. Corollary 4.1(i): for almost every $t$, $\frac{d}{dt}f(x(t))=\langle\dot x(t),x^*\rangle$ for every $x^*\in\partial f(x(t))$.
2. Corollary 4.1(iii): every trajectory extends to a maximal one on $[0,+\infty)$ with $\dot x\in L^2$.
3. Corollary 4.2: $\|\dot x(t)\|=m_f(x(t))$ and $\frac{d}{dt}f(x(t))=-m_f(x(t))^2$ almost everywhere.
4. Inequality (20): the Łojasiewicz inequality holds around every point of $\operatorname{dom}\partial f$.
5. Theorem 4.5: bounded maximal trajectories have finite length $\int_0^\infty\|\dot x\|<\infty$ and converge to a critical point.
6. The tail bound $\int_t^\infty\|\dot x\|\le\frac{c}{1-\theta}(f(x(t))-f(a))^{1-\theta}$.
7. Inequality (27): $\int_t^\infty\|\dot x\|\le\frac{c^{1/\theta}}{1-\theta}\|\dot x(t)\|^{(1-\theta)/\theta}$ for almost every large $t$.

Significance

Theorem 4.5 says that for convex or lower-$C^2$ subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at $\theta=\tfrac12$, polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.

On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on $[0,T)$, a chain rule for $f\circ x$ along absolutely continuous curves, and a comparison lemma for the differential inequality $\dot\sigma\le-L\sigma^\alpha$. The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.

Difficulty

Compactness gives cluster points of a bounded trajectory, and the decrease of $f$ gives convergence of $f(x(t))$. Neither gives convergence of $x(t)$. The usual first idea, that $\int_0^\infty\|\dot x\|^2<\infty$ forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control $\int\|\dot x\|$ rather than $\int\|\dot x\|^2$. That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: $f\circ x$ is differentiable almost everywhere with derivative $\langle\dot x,x^*\rangle$ for every $x^*\in\partial f(x(t))$, which relies on $\partial f=\hat\partial f$ for convex and lower-$C^2$ functions. Global existence on $[0,+\infty)$ (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.

Formalization scope

Space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes $-\infty$. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope $m_f$ is valued in $[0,+\infty]$. The Łojasiewicz inequality is encoded as $|f(y)-f(a)|^\theta\le C\|v\|$ for $y$ near $a$ and every $v\in\partial f(y)$, which is the bounded ratio under the paper's conventions. Times are real numbers and $T\in[0,+\infty]$. Curves are functions $\mathbb R\to\mathbb R^n$ whose values outside $[0,T)$ are irrelevant. "Absolutely continuous on $[0,T)$" means absolutely continuous on every compact $[0,b]\subseteq[0,T)$. Velocities appear only "for almost every $t$". Lengths are lower Lebesgue integrals $\int^-\|\dot x\|$ in $[0,+\infty]$, never Bochner integrals (which would vanish for a non-integrable speed).

Two trivializations are ruled out. Maximality is a hypothesis and $T=+\infty$ is a conclusion: assuming $T=+\infty$ would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on $\mathbb R_+$ with $\dot{\hat x}\in L^2$", because the printed $\hat x\in W^{1,2}(\mathbb R_+)$ would fail for any trajectory with nonzero limit.

Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower-$C^2$ functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.

Selected references

• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
• H. Brézis, Opérateurs maximaux monotones et semi-groupes de contractions dans les espaces de Hilbert, North-Holland, 1973.
• J.-P. Aubin, A. Cellina, Differential Inclusions, Springer, 1984. https://doi.org/10.1007/978-3-642-69512-4
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116 (2009) 5–16. https://doi.org/10.1007/s10107-007-0133-5