The OR Formalization Drive

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output $y = Cx$ is measured, and the controller is restricted to a static feedback $u = -Ky$. For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix $K$.

Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$, $B\in\mathbb R^{n\times m}$, $C\in\mathbb R^{r\times n}$ and weights $Q\in\mathbb R^{n\times n}$, $R\in\mathbb R^{m\times m}$, and an initial-state covariance $\Sigma\in\mathbb R^{n\times n}$. A gain is a matrix $K\in\mathbb R^{m\times r}$, and the closed-loop matrix is $A_K = A - BKC$. A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is

$$\mathcal S = \{K\in\mathbb R^{m\times r} : A_K \text{ is Hurwitz}\}.$$

For $K\in\mathcal S$ let $X(K)$ be the unique solution of the Lyapunov equation

$$A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,$$

and define the cost $f(K)=\mathrm{Tr}\big(X(K)\Sigma\big)$, the expected integrated quadratic cost of the closed loop from a random initial state with covariance $\Sigma$. With $Y(K)$ the solution of $A_KY+YA_K^\top+\Sigma=0$, the gradient of $f$ in the Frobenius inner product is

$$\nabla f(K)=2\big(RKC-B^\top X(K)\big)Y(K)C^\top .$$

A known stabilizing gain $K_0\in\mathcal S$ is given, and $\mathcal S_0=\{K\in\mathcal S: f(K)\le f(K_0)\}$ is its sublevel set. The standing assumptions are $Q,R,\Sigma\succ0$, $\operatorname{rank}C=r$ and $B\neq0$. State feedback (SLQR) is the case $C=I$.

The gradient method with step sizes $\gamma_j$ is

$$K_{j+1}=K_j-\gamma_j\nabla f(K_j),\qquad j\ge0 .$$

A number $L>0$ is a smoothness constant if $\|\nabla f(K)-\nabla f(K')\|_F\le L\|K-K'\|_F$ for all $K,K'\in\mathcal S_0$.

Formalization targets

Goal: Theorem 4.2 for state feedback

For $C=I$, an optimal gain $K_*\in\mathcal S$, and any smoothness constant $L$:

1. if $0<\gamma_j\le 2/L$ for all $j$, then every $K_j\in\mathcal S_0$ and

$$f(K_{j+1})\le f(K_j)-\gamma_j\Big(1-\frac{L\gamma_j}{2}\Big)\|\nabla f(K_j)\|_F^2 ;$$

2. if $0<\varepsilon_1\le\gamma_j\le 2/L-\varepsilon_2$ with $\varepsilon_2>0$, then $\nabla f(K_j)\to0$,

$$\min_{0\le j\le k}\|\nabla f(K_j)\|_F^2\le\frac{f(K_0)}{c_1k}\quad(k\ge1),\qquad c_1=\frac{\varepsilon_1\varepsilon_2L}{2},$$

and there are $c\ge0$, $0\le q<1$ with $\|K_j-K_*\|_F\le c\,q^j$.

Milestones

In attack order:

• Appendix A lemmas. Trace duality of dual Lyapunov equations (Lemma A.1), the trace sandwich (Lemma A.4), and eigenvalue lower bounds for Lyapunov solutions (Lemma A.5).
• Coercivity and existence. Coercivity of $f$ with the lower bounds (3.1)–(3.2) (Lemma 3.8), boundedness of $\mathcal S_0$ (Corollary 3.9), and existence of a minimizer (Corollary 3.10).
• Smoothness. The gradient formula (Lemma 3.11) and existence of a smoothness constant on $\mathcal S_0$ (Theorem 3.15, qualitative form).
• Gradient domination for state feedback. Lemmas C.2, C.3 and C.1, and the LPL inequality with the explicit constant (3.11):

$$\tfrac12\|\nabla f(K)\|_F^2\ge\mu\big(f(K)-f(K_*)\big),\qquad K\in\mathcal S_0 \qquad\text{(Theorem 3.17)}.$$

• Theorem 4.2 for output feedback. Descent and stationarity, parts 1 and 2 without the linear rate, for general $C$.

Significance

The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain $\mathcal S$ is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.

The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in $\mathcal S_0$) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.

Difficulty

The standard descent-lemma argument assumes $f$ is defined and $L$-smooth on the whole space. Here $f$ is defined only on $\mathcal S$, and it is not smooth on all of $\mathcal S$: it blows up at the boundary. A gradient step from a point of $\mathcal S_0$ could in principle jump out of $\mathcal S$, where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside $\mathcal S_0$, so the argument must show that the whole segment from $K_j$ to $K_{j+1}$ stays in $\mathcal S_0$ before the descent inequality can be used on it. That requires coercivity, compactness of $\mathcal S_0$ and an exit-time argument. For the linear rate, gradient domination has to be established on $\mathcal S_0$ with constants controlled by $f(K_0)$, and passing from function values to distances to $K_*$ needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for $C=I$.

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. $X(K)$, $Y(K)$ are "the unique solution of the Lyapunov equation, $0$ if there is none or several"; this junk value is never used, because every statement evaluates $f$ and $\nabla f$ only at gains proved or assumed to lie in $\mathcal S$. The iterates' membership in $\mathcal S_0$ is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. $\nabla f$ is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. $\|\cdot\|_F$ is $\sqrt{\sum M_{ij}^2}$, $\|\cdot\|$ is the spectral (operator) norm, and $\lambda_1,\lambda_n$ are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance $r=n$, $C=1$. In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because $c$ is existential. The minimum over $0\le j\le k$ requires $k\ge1$.

Deviations from the printed text, each recorded in the item's Formalization Note:

• The smoothness constant. The explicit $L$ of (3.8) is false as printed (for $n=m=1$, $A=0$, $B=100$, $Q=100$, $R=10^{-3}$, $\Sigma=0.1$, $K_0=10^{-6}$, one has $f''(K_0)=2L$). The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$, which is the paper's definition of $L$-smoothness (§3.6) and all that its proof uses. Theorem 3.15 enters only as "some such $L>0$ exists".
• Lemma C.1. It is stated with $\lambda_1^2(\Sigma)$ in the denominator, as its proof concludes and as (3.11) requires.
• Lemma A.5. It is stated for $A^\top X+XA+Q=0$; the printed $-Q$ admits no positive definite solution.
• The gain space. $\mathcal S\subseteq\mathbb R^{m\times r}$, where p. 3 prints $\mathbb R^{m\times n}$.

Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59(5), 2021; preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
• M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
• W. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15(1), 1970. https://doi.org/10.1109/TAC.1970.1099363
• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5, 1960.

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost of state and input. When the full state is measured, the optimal law is a static linear feedback $u = -Kx$ obtained from an algebraic Riccati equation. When only an output $y = Cx$ is measured, the optimal static output feedback $u = -Ky$ has no closed form, and the problem is nonconvex. In both cases the cost can be written as a function $f(K)$ of the gain alone, which makes it natural to minimize $f$ by gradient methods directly in the space of gains. This view goes back to Levine and Athans (1970) for output feedback and was revived in reinforcement learning by Fazel, Ge, Kakade and Mesbahi (2018), who proved global convergence of policy gradient for discrete-time state-feedback LQR.

Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021) carry out this program for the continuous-time problem. They show that $f$ is coercive, that it is $L$-smooth on every sublevel set, and that under state feedback it satisfies a gradient-domination (Łojasiewicz–Polyak) inequality. From these properties they derive convergence of the continuous gradient flow and of the discrete gradient method. This mission formalizes the continuous part, Theorem 4.1.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$, $B\in\mathbb R^{n\times m}$, $C\in\mathbb R^{r\times n}$ and symmetric positive definite weights $Q\in\mathbb R^{n\times n}$, $R\in\mathbb R^{m\times m}$ and covariance $\Sigma\in\mathbb R^{n\times n}$. A gain is $K\in\mathbb R^{m\times r}$, and the closed-loop matrix is $A_K = A - BKC$. A square matrix is Hurwitz if all its eigenvalues have negative real part. The stabilizing set is

$$\mathcal S = \{K : A_K \text{ is Hurwitz}\}.$$

For $K\in\mathcal S$, let $X(K)$ and $Y(K)$ be the unique solutions of the Lyapunov equations

$$A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,\qquad A_KY + YA_K^\top + \Sigma = 0 .$$

The LQR cost is $f(K) = \mathrm{Tr}(X(K)\Sigma)$. It equals the expected infinite-horizon quadratic cost when the initial state has covariance $\Sigma$. Its gradient with respect to the Frobenius inner product $\langle M,N\rangle = \mathrm{Tr}(M^\top N)$ is

$$\nabla f(K) = 2\,(RKC - B^\top X(K))\,Y(K)\,C^\top .$$

Given a known stabilizing gain $K_0\in\mathcal S$, the sublevel set is $\mathcal S_0 = \{K\in\mathcal S : f(K)\le f(K_0)\}$. The gradient flow is the ODE

$$\dot K(t) = -\nabla f(K(t)),\qquad K(0) = K_0 .$$

State feedback (SLQR) is the case $C = I$; there $f$ is written $f_S$, and $K_*$ denotes a minimizer of $f_S$ on $\mathcal S$. Norms: $\|\cdot\|_F$ is the Frobenius norm and $\|\cdot\|$ the spectral norm. $\lambda_1(M)$ is the smallest eigenvalue of a symmetric $M$.

Formalization targets

Goal: Theorem 4.1 for state feedback

For $C=I$, let $L>0$ be a Lipschitz constant of $\nabla f$ on $\mathcal S_0$ and let $\mu$ be the constant (3.11),

$$\mu = \frac{\lambda_1(R)\lambda_1^2(\Sigma)\lambda_1(Q)}{8f_S(K_*)\big(\|A\| + \|B\|^2 f_S(K_0)/(\lambda_1(\Sigma)\lambda_1(R))\big)^2}.$$

Then the flow has a solution on $[0,\infty)$, and every solution stays in $\mathcal S_0$, has $f(K_t)$ nonincreasing, has $\nabla f(K_t)\to0$ and $\min_{0\le t\le T}\|\nabla f(K_t)\|_F^2\le f(K_0)/T$, and

$$\|K_t - K_*\|_F \le \frac{\sqrt{2L(f(K_0)-f(K_*))}}{\mu}\,e^{-\mu t}\qquad(t\ge0).$$

Milestones

In attack order:

1. Existence of a minimizer (Corollary 3.10).
2. The gradient formula (Lemma 3.11).
3. Existence of a Lipschitz constant of $\nabla f$ on $\mathcal S_0$ (Theorem 3.15, qualitative).
4. The gradient-domination inequality $\tfrac12\|\nabla f_S(K)\|_F^2\ge\mu(f_S(K)-f_S(K_*))$ on $\mathcal S_0$ (Theorem 3.17).
5. The energy identity $\tfrac{d}{dt}f(K_t) = -\|\nabla f(K_t)\|_F^2$.
6. The integral bound of Appendix D.1.
7. The output-feedback part of Theorem 4.1 (general $C$ with $\operatorname{rank} C = r$): existence, invariance of $\mathcal S_0$, monotonicity and (4.2).

Significance

The theorem certifies a simple, model-based procedure: start from any stabilizing gain and follow the negative gradient of the cost. The iterate never loses stability, and it converges exponentially to the optimal gain. The same happens for state feedback even though neither $f$ nor $\mathcal S$ is convex. For output feedback it guarantees convergence to stationarity with an explicit $O(1/T)$ rate. The continuous-time result is the template for the discrete gradient method of the same paper (Theorem 4.2) and for policy-gradient analyses of LQR in learning-based control.

The result is proved in the paper. The paper writes out the proof of (4.2) in Appendix D.1. It describes the whole proof as a replica of Theorems 8 and 9 of Polyak 1963, which treat functions satisfying the Łojasiewicz–Polyak inequality on the whole space. No machine-checked version of any of these statements is known. A formal proof would give the first verified treatment of LQR as an optimization problem over gains. It needs Lyapunov equations, the stabilizing set and the cost, together with the analytic facts on which the policy-gradient literature rests: coercivity, smoothness on sublevel sets, and gradient domination.

Difficulty

The obvious argument is the textbook convergence proof for gradient flows of smooth functions satisfying the Łojasiewicz–Polyak inequality. That proof assumes the function is defined and smooth on the whole space. Here $f$ lives only on the open set $\mathcal S$, blows up at its boundary, is unbounded on $\mathcal S$ and is not globally $L$-smooth. The Łojasiewicz–Polyak inequality holds only on $\mathcal S_0$, with a constant that depends on $K_0$. The work therefore lies in keeping the trajectory inside $\mathcal S_0$ and showing it exists for all time. This requires compactness of $\mathcal S_0$ (coercivity of $f$) and a positive distance from $\mathcal S_0$ to the boundary of $\mathcal S$. Local ODE existence alone gives neither. The explicit constant $\mu$ additionally requires lower bounds on solutions of Lyapunov equations and an upper bound on $\|K\|_F$ over $\mathcal S_0$.

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every complex eigenvalue of the complexified matrix has negative real part. $X(K)$ and $Y(K)$ are the unique solutions of their Lyapunov equations. Where the solution is not unique (possible only off $\mathcal S$) they take the value $0$, and no statement uses these off-$\mathcal S$ values. $\nabla f$ is defined by formula (3.3), and Lemma 3.11 states that it is the Fréchet derivative with respect to the Frobenius inner product. A solution of the flow is a curve with $K(0)=K_0$ that stays in $\mathcal S$ for $t\ge0$. Its entries have the prescribed derivative within $[0,\infty)$. Global existence and invariance of $\mathcal S_0$ are conclusions, never hypotheses. Assuming a global solution, or a solution confined to $\mathcal S_0$, would trivialize the theorem, and that encoding is excluded. The case $C=I$ is a matrix argument $C$ with $C=1$. $\lambda_1$ is the minimum of the (unsorted) eigenvalues, and the spectral norm is $\sqrt{\lambda_{\max}(M^\top M)}$. "Monotone decreasing" is rendered as nonincreasing. $\min_{0\le t\le T}$ is rendered as the existence of a point of $[0,T]$ where the bound holds.

The standing assumptions of p. 3 are hypotheses wherever they apply: $K_0\in\mathcal S$, $Q,R,\Sigma\succ0$, $\operatorname{rank}C=r$, and $B\ne0$. Deviations from the printed paper:

• The paper's explicit Lipschitz constant (3.8) is false as printed; the planning notes record counterexamples for both output and state feedback. The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$, which is the paper's own definition of $L$-smoothness (§3.6). Theorem 3.15 enters only in its qualitative form, as the existence of such an $L$.
• The set-builder for $\mathcal S$ on p. 3 writes $\mathbb R^{m\times n}$; gains are $m\times r$.
• The optimal gain $K_*$ is a hypothesis (its existence is Corollary 3.10), and $f(K_*)>0$ is not assumed.

A complete development needs the following: Lyapunov equations and their solution theory (uniqueness, positivity, integral representation), continuity and differentiability of $K\mapsto X(K)$ on $\mathcal S$, coercivity of $f$, global existence for ODEs confined to a compact invariant set, and the Łojasiewicz–Polyak argument for flows on a subset. The Lyapunov and stabilizing-set layer is reusable across control missions. Proofs of any milestone, and of auxiliary lemmas such as Lemmas 3.8, A.5, C.1–C.3, are welcome.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59 (2021); preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
• M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
• W. S. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15 (1970). https://doi.org/10.1109/TAC.1970.1099363
• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for the minimisation of functionals, USSR Comput. Math. Math. Phys. 3 (1963), 864–878. https://doi.org/10.1016/0041-5553(63)90382-3

Motivation

Vehicle routing problems ask for minimum-cost vehicle routes that deliver goods from a depot to a set of customers. In the split-delivery vehicle routing problem with time windows (SDVRPTW) a customer's demand may be served by several vehicles, and each customer must be visited inside a prescribed time window. Allowing split deliveries matters in practice: for the variant without time windows, Dror and Trudeau (1989) showed empirically that splitting can save substantially, and Archetti, Savelsbergh and Speranza (2006) proved the savings can reach 50%.

Exact methods for the SDVRPTW are branch-and-price algorithms, and they rely on structural properties of optimal solutions to prune the search. Desaulniers (Operations Research 58(1), 2010) collects these properties in §2 of his paper and uses the strongest one, Corollary 2, as a family of valid inequalities (constraint (7)) in his branch-and-price-and-cut method.

Timeline (as reported by Desaulniers 2010, §§1–2).

• 1989–1990. Dror and Trudeau prove, for the SDVRP without time windows and with the triangle inequality, that some optimal solution has no two routes sharing more than one split customer.
• 2006. Gendreau, Dejax, Feillet and Gueguen observe that the property holds with time windows, derive the arc-based Corollary 1, and remark that elementary routes suffice (Remark 1).
• 2010. Desaulniers strengthens Corollary 1 to pairs of reverse arcs (Corollary 2) and exploits it as cutting planes.

Setting

An instance has $n$ customers $\mathcal N$, a start depot $0$ and an end depot $n+1$ (the same location at the beginning and end of the planning horizon), and the following data: a vehicle capacity $Q > 0$; a demand $d_i > 0$ for each customer, which may exceed $Q$; a time window $[e_v, l_v]$ for each node, shared by the two depot copies; nonnegative travel times $t_{vw}$, which include the service time at $v$; and nonnegative costs $c_{vw}$. The arc set $\mathcal A$ contains the idle arc $(0, n+1)$ and every arc $(v, w)$, $v \ne w$, with $e_v + t_{vw} \le l_w$. The triangle inequality $t_{vx} \le t_{vw} + t_{wx}$, $c_{vx} \le c_{vw} + c_{wx}$ is assumed throughout.

A route is a walk $0 \to v_1 \to \dots \to v_m \to n+1$ along arcs of $\mathcal A$, customers possibly repeated, with service start times inside the time windows that respect travel times (waiting is allowed), and nonnegative quantities delivered at its visits whose total is at most $Q$. Its cost is the sum of its arc costs. A solution is a finite family of routes, one per vehicle, with no bound on their number; it is feasible if every customer $i$ receives in total at least $d_i$, and optimal if it is feasible and no feasible solution costs less. For customers $i, j$, let $x_{ij}$ be the number of times arc $(i, j)$ is traversed, summed over all routes of a solution, and let $\mathcal A(\mathcal N) = \mathcal A \cap (\mathcal N \times \mathcal N)$.

Formalization targets

All four statements assume the triangle inequality and that the instance has a feasible solution, and assert the existence of an optimal solution with a structural property.

Goal: Corollary 2 (p. 181)

$$\exists \text{ optimal solution with } x_{ij} + x_{ji} \le 1 \quad \text{for all } (i,j) \in \mathcal A(\mathcal N).$$

The two arcs of a pair of reverse customer arcs are used at most once in total. This is the form constraint (7) of the paper gives to the corollary.

Milestones

1. Remark 1. Some optimal solution has only elementary routes: no route visits a customer twice.
2. Theorem 1. Some optimal solution has no two distinct routes with two customers in common.
3. Corollary 1. Some optimal solution has $x_{ij} \le 1$ for all $(i, j) \in \mathcal A(\mathcal N)$.

Significance

The result. Corollary 2 turns a property of optimal solutions into linear inequalities on arc-flow variables. Adding them to the arc-flow formulation cuts off fractional points of its linear relaxation while keeping an optimal integer solution, which is how Desaulniers uses them. Remark 1 justifies pricing only elementary routes in column generation. Theorem 1 is the combinatorial fact underneath both corollaries and is reused throughout the split-delivery literature.

Formalizing it. The four results are proved in the literature (Dror–Trudeau; Gendreau et al. 2006); Desaulniers states them without proof. No machine-checked version exists. This mission produces a reusable Lean model of the SDVRPTW (instances, arc sets, feasible routes with schedules and delivery patterns, solutions, optimality) and checked proofs of these properties, including the existence of an optimal solution, which the paper takes for granted.

Difficulty

The obvious argument is local: take an optimal solution that violates the property, shift quantities between two routes, remove a visit, and shortcut. Three points make this less routine than it sounds. First, the statements are existential: each exchange must keep the solution optimal and not reintroduce a violation already removed, so one needs a termination measure that decreases under every exchange (Corollary 2 needs elementarity and the Theorem 1 property simultaneously, not two separate optimal solutions). Second, removing a visit is feasible only because the arc set is defined by time windows: the shortcut arc $(v, w)$ must be shown to exist from the schedule and the triangle inequality on travel times, and the new schedule must be built explicitly. Third, the feasible set is infinite (real quantities, unbounded walks, unbounded number of vehicles), so the existence of an optimal solution is itself a statement to prove, not a hypothesis.

Formalization scope

Namespace SplitDeliveryVRPTW.Known. Nodes are the inductive type Node n (start, cust i for i : Fin n, finish). All quantities, times and costs are real. The arc set is exactly the set the paper defines (read as "if and only if"), with arcs into the start depot and out of the end depot excluded. The triangle inequality for $t$ is imposed on pairwise distinct nodes and for $c$ on triples of arcs, where the paper's data is defined. A route is a customer list (repetitions allowed) with a time function over path positions and a quantity function over visits. A solution is an indexed family Fin m → Route I, so identical routes may appear twice. Demand satisfaction uses $\ge$, as constraint (2) does. The per-vehicle bound $\min\{d_i, Q\}$ of constraint (14) is omitted because it changes neither the feasible route patterns nor the costs.

Explicit readings of imprecise phrases:

• "split customer", "in common" (Theorem 1) are undefined in the paper. A customer two distinct routes visit is split, and the routes have it in common. This visit-based reading is at least as strong as a delivery-based one.
• Corollary 2's wording "at most one arc in set $\mathcal A^*_{ij}$ appears at most once" is read through constraint (7): the total number of traversals of the arcs of $\mathcal A^*_{ij}$ is at most one. It is stated in the equivalent form free of the choice of $\mathcal A^*(\mathcal N)$.
• "there exists an optimal solution" is conditional on feasibility, which is the hypothesis added.

Ruled-out trivializations: routes are not restricted to elementary walks (that would make Remark 1 definitional), solutions are not sets (that would forbid duplicate routes), optimality compares against solutions with any number of routes and any visit pattern, "split" is never counted over visits by the same route, capacity and time windows are part of route feasibility, and deliveries occur only at visits.

Useful infrastructure, reusable beyond this mission: shortcut lemmas for feasible routes (removing a visit), exchange lemmas between two routes, and existence of an optimum for split-delivery routing. Contributions of any of these as separate lemmas are welcome.

Selected references

• G. Desaulniers, Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows, Operations Research 58(1):179–192, 2010. https://doi.org/10.1287/opre.1090.0713
• M. Dror, P. Trudeau, Savings by split delivery routing, Transportation Science 23(2):141–145, 1989. https://doi.org/10.1287/trsc.23.2.141
• M. Dror, P. Trudeau, Split delivery routing, Naval Research Logistics 37(3):383–402, 1990. https://doi.org/10.1002/nav.3800370304
• M. Gendreau, P. Dejax, D. Feillet, C. Gueguen, Vehicle routing with time windows and split deliveries, Technical Report 2006-851, Laboratoire Informatique d'Avignon, 2006.
• C. Archetti, M. W. P. Savelsbergh, M. G. Speranza, Worst-case analysis for split delivery vehicle routing problems, Transportation Science 40(2):226–234, 2006. https://doi.org/10.1287/trsc.1050.0117

Motivation

A convex risk measure assigns to a bounded financial position $X$ (a random net payoff) a number $\rho(X)$, interpreted as the capital that must be added to $X$ to make it acceptable. The axiomatic theory began with coherent risk measures (Artzner, Delbaen, Eber and Heath, 1999) and was extended to convex ones by Föllmer and Schied (2002) and Frittelli and Rosazza Gianin (2002). Its central structural result is a robust representation: a convex risk measure that is continuous from above equals a worst case of expected losses over a family of probabilistic models, each penalized by how implausible it is.

Regulators and risk managers do not assess positions once and for all; they reassess them as information arrives. Detlefsen and Scandolo (2005) extend the representation to conditional risk measures, whose value $\rho(X)$ is itself a random variable measurable with respect to the information available to the agent. This is the building block of dynamic (time-consistent) risk measurement, studied in later work on dynamic risk measures and backward stochastic differential equations.

Timeline. Artzner et al. (1999): coherent risk measures on finite $\Omega$. Delbaen (2002): coherent risk measures on general probability spaces, Fatou property. Föllmer–Schied (2002) and Frittelli–Rosazza Gianin (2002): convex risk measures and their robust representation; Föllmer–Schied, Stochastic Finance, Theorem 4.26 (2002 edition) for $L^\infty$ with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$ describing the available information. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$-measurable part; every (in)equality between random variables holds $P$-almost surely.

A map $\rho:L^\infty\to L^\infty_{\mathcal G}$ is a conditional convex risk measure if $\rho(0)=0$ and, for $X,Y\in L^\infty$:

• (conditional translation invariance) $\rho(X+Z)=\rho(X)-Z$ for every $Z\in L^\infty_{\mathcal G}$;
• (monotonicity) $X\le Y$ implies $\rho(X)\ge\rho(Y)$;
• (conditional convexity) $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for every $\Lambda\in L^\infty_{\mathcal G}$ with $0\le\Lambda\le1$.

The admissible models are

$$\mathcal P_{\mathcal G}=\{Q \text{ probability on }(\Omega,\mathcal F): Q\ll P,\ Q(A)=P(A)\text{ for all }A\in\mathcal G\}.$$

For a family $\mathcal X$ of $[-\infty,+\infty]$-valued random variables, the essential supremum $\operatorname{ess.sup}\mathcal X$ is the $P$-a.s. smallest random variable that dominates every member $P$-a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.

A map $\rho$ is representable if there is a penalty $\alpha:\mathcal P_{\mathcal G}\to L^0_{\mathcal G}([0,+\infty])$ with

$$\rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha(Q)\},\qquad X\in L^\infty .$$

The minimal penalty is $\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\}$. $\rho$ is continuous from above if $X_n\searrow X$ $P$-a.s. implies $\rho(X_n)\nearrow\rho(X)$ $P$-a.s.

Formalization targets

Goal: Theorem 3.2

For a conditional convex risk measure $\rho$, the following are equivalent:

$$\text{(a) } \rho \text{ continuous from above}\iff\text{(b) } \rho\text{ representable}\iff\text{(c) } \rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}.$$

Milestones

• Theorem A.1: existence and a.s. uniqueness of the essential supremum; an increasing sequence converging to it for upward directed families.
• Lemma A.2: $E_P(\operatorname{ess.sup}\mathcal X)=\sup_{X\in\mathcal X}E_PX$ for upward directed $\mathcal X$.
• The easy inequality $\rho(X)\ge\operatorname{ess.sup}_{Q}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}$.
• The unconditional representation (Föllmer–Schied, Theorem 4.26) of a convex risk measure $\rho_0:L^\infty\to\mathbb R$ continuous from above: $\rho_0(X)=\sup_{Q\ll P}\{-E_QX-\alpha^*_0(Q)\}$.
• For $\rho_0=E_P[\rho(\cdot)]$: $\alpha^*_0(Q)<\infty$ forces $Q\in\mathcal P_{\mathcal G}$.
• The family $B_Q=\{-E_Q(X\mid\mathcal G)-\rho(X):X\in L^\infty\}$ is upward directed.
• $E_P[\alpha^*(Q)]=\alpha^*_0(Q)$ for $Q\in\mathcal P_{\mathcal G}$.
• Representable implies continuous from above.
• Remark 3.3: $\alpha^*\le\alpha$ for every penalty $\alpha$, and $\alpha^*(Q)=\operatorname{ess.sup}_{X\in\mathcal A_\rho}\{-E_Q(X\mid\mathcal G)\}$.

Significance

The result. Theorem 3.2 shows that a conditional convex risk measure is determined by a random penalty on the models consistent with the available information, exactly when it satisfies a sequential continuity condition. The representation is the input for the paper's later sections: the conditional entropic risk measure, whose minimal penalty is the conditional relative entropy, and the consistency of dynamic risk measures via Lemma 3.4, which is expressed through the minimal penalty. The restriction to $\mathcal P_{\mathcal G}$ has an interpretation: the more information, the fewer models can enter the worst case.

Formalizing it. The theorem has been proved in the literature since 2005; to our knowledge neither it nor its unconditional counterpart has a machine-checked proof. The mission produces an essential supremum of arbitrary families of extended random variables with its existence theorem, the exchange of expectation and essential supremum for directed families, and the unconditional Föllmer–Schied representation on $L^\infty$. The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.

Difficulty

The obvious route, applying the unconditional representation pathwise or $\omega$ by $\omega$, fails: $\rho(X)(\omega)$ is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on $Q$, of which there are uncountably many. The essential supremum is what turns an uncountable supremum of classes into a well-defined class, and passing expectations through it requires directedness. The unconditional step itself (continuity from above implies the dual representation) rests on a Krein–Šmulian / weak* closedness argument on $L^\infty$, which is not available off the shelf.

Formalization scope

• Payoffs are real functions $\Omega\to\mathbb R$ with MemLp X ⊤ P; $\rho$ is a map $(\Omega\to\mathbb R)\to(\Omega\to\mathbb R)$ constrained only on $L^\infty$. Because it acts on functions, $\rho$ is required to respect $P$-a.s. equality, and $\rho(X)$ is required to be $\mathcal G$-strongly measurable and essentially bounded; the paper's $\rho$ acts on classes, so this adds nothing in substance. $\mathcal G$ is a MeasurableSpace m with m ≤ mΩ.
• Translation invariance and convexity quantify over $\mathcal G$-measurable $Z$ and $\Lambda$ (not constants). $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ — equality on $\mathcal G$, not mutual absolute continuity.
• $E_Q(X\mid\mathcal G)$ is Mathlib's Q[X | m]; it is $\mathcal G$-measurable, hence determined $P$-a.s. for $Q\in\mathcal P_{\mathcal G}$.
• Extended values live in EReal; penalties are ENNReal-valued and coerced, so only (real) $-(+\infty)=-\infty$ occurs, never $+\infty-(+\infty)$.
• The essential supremum is a predicate IsEssSup P F Z (a.e. upper bound of every member, a.e. below every a.e.-measurable a.e. upper bound). The minimal penalty is a predicate IsMinimalPenalty on a candidate; statement (c) of the goal asserts that a $\mathcal G$-measurable $[0,+\infty]$-valued essential supremum of $B_Q$ is a penalty for $\rho$.
• Continuity from above: $X_n,X\in L^\infty$, $(X_n)$ a.s. non-increasing and a.s. convergent to $X$ implies $(\rho(X_n))$ a.s. non-decreasing and a.s. convergent to $\rho(X)$. It is not norm or weak* continuity.
• Lemma A.2's "provided the expectations exist" is pinned as: each member has an expectation in $[-\infty,+\infty]$ and some member has integrable negative part (without the latter the lemma is false). Theorem A.1's directed part assumes a nonempty family. The acceptance set of Remark 3.3 is $\{X\in L^\infty:\rho(X)\le0\}$ (the paper's $L^\infty_{\mathcal G}$ on p. 4 is a misprint).
• Ruled out: an essential supremum defined as a pointwise ⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all $Q\ll P$ or to the $Q$ equivalent to $P$; each of these changes statement (b) or makes it vacuous.
• Needed infrastructure: essential suprema of families, extended expectations with monotone convergence, conditional expectation under a change of measure agreeing on $\mathcal G$, and the $L^\infty$–$L^1$ duality behind Föllmer–Schied 4.26. The essential-supremum layer and the unconditional representation are reusable in any mission on risk measures or robust optimization; contributions to either are welcome.

Selected references

• K. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized here; journal version: Finance and Stochastics 9(4), 539–561, 2005, https://doi.org/10.1007/s00780-005-0159-6)
• H. Föllmer, A. Schied, Stochastic Finance — An Introduction in Discrete Time, de Gruyter Studies in Mathematics 27, 2002. https://doi.org/10.1515/9783110198065
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4), 429–447, 2002. https://doi.org/10.1007/s007800200072
• M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking and Finance 26, 1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002. https://doi.org/10.1007/978-3-662-04790-3_1