Operations Research

Motivation

Prescriptive analytics chooses a decision $z$ from data after observing a context $x_0$: a retailer sets an order quantity after seeing the weather forecast, a hospital schedules staff after seeing the day of the week. A common recipe estimates the expected cost of each decision from the training observations closest to $x_0$ (nearest neighbours, or a kernel-weighted Nadaraya–Watson average) and then minimizes that estimate (Bertsimas and Kallus, 2020). The decision that minimizes an estimate tends to look better on the training data than it is: its estimated cost is optimistically biased. Bertsimas and Van Parys (arXiv:1711.09974v2) measure that optimism on resampled data. Bootstrap data are $n$ independent draws from the training distribution, in the sense of Efron (1979). A cost budget computed on the training data disappoints when the estimate on a bootstrap sample exceeds it. The paper replaces the nominal estimate by a robust budget, a worst case over all distributions within relative-entropy distance $r$ of the training distribution. Its Theorem 6 bounds the probability of disappointment by an explicit sum of exponentials in $n$.

This mission formalizes that theorem, together with the structural results its proof rests on and the Nadaraya–Watson special case, Corollary 2. The same paper's dual reformulation of the budget (Lemma 2) and its optimality statement for the relative entropy (Proposition 1) are the subject of two sibling missions.

Setting

The $n$ training points have a finite set $\Omega_n$ of distinct values. A distribution on $\Omega_n$ is a vector $D=(D_i)_{i\in\Omega_n}$ in the standard simplex; these form $\mathcal D_n$. The training distribution $D_{\mathrm{tr}}\in\mathcal D_n$ gives every point of $\Omega_n$ positive mass. The bootstrap distributions are

$$\mathcal D_{n,n}=\{D\in\mathcal D_n:\ nD_i\in\{0,1,\dots,n\}\ \forall i\}.$$

These are the possible empirical distributions $D_{\mathrm{bs}[n]}$ of $n$ independent draws from $D_{\mathrm{tr}}$.

Around the context $x_0$ the points of $\Omega_n$ are grouped into nested neighbourhoods $\emptyset=N^0\subseteq N^1\subseteq\dots\subseteq N^n=\Omega_n$. Each point $i$ carries a positive weight $w_i$ and, for a decision $z$, a loss $\ell_i=L(z,\bar y_i)$. Fix $k\in\{1,\dots,n\}$. The estimator (18) of a distribution $D$ averages the loss with weights $w_iD_i$ over the smallest neighbourhood $N^{j}$ with $D$-mass at least $k/n$. For $j\in[n]$, the partial estimator $E^{n,j}_D$ is the value of the linear program (22). Its domain is contained in

$$\mathcal D^j_n=\Big\{D\in\mathcal D_n:\ \sum_{i\in N^{j-1}}D_i\le\tfrac{k-1}{n},\ \ \tfrac kn\le\sum_{i\in N^j}D_i\Big\},$$

and off that domain $E^{n,j}_D=-\infty$.

The bootstrap distance is the relative entropy

$$B(D,D')=\sum_{i}D_i\log\frac{D_i}{D'_i}.$$

The partial robust budgets are $c^j_n=\sup\{E^{n,j}_D:\ D\in\mathcal D_n,\ B(D,D_{\mathrm{tr}})\le r\}$, the robust budget is $\bar c_n=\max_{j\in[n]}c^j_n$ (26), and the minimum radii are $r^j_n=\inf\{B(D,D_{\mathrm{tr}}):D\in\mathcal D^j_n\}$ (29).

Formalization targets

Goal: Theorem 6 (p. 15)

For every decision $z$,

$$\mathbb P\Big[E^n_{D_{\mathrm{bs}[n]}}[L(z,y)\,|\,x=x_0]>\bar c_n(z)\Big]\ \le\ \sum_{j\in[n]}\exp\big(-n\cdot\max\{r,r^j_n\}\big).$$

The bound holds for every $n$, $k$, neighbourhood chain, weight vector and radius, with no asymptotics.

Milestones

1. The domain inclusion (23), with $E^{n,j}_D=-\infty$ off $\mathcal D^j_n$ (p. 11).
2. The closed form of $E^{n,j}_D$ on $\mathcal D^j_n$ as a weighted average over $N^j$ (B.1, p. 26).
3. The sets $\mathcal D^j_n\cap\mathcal D_{n,n}$, $j\in[n]$, partition $\mathcal D_{n,n}$ (B.1, p. 26).
4. Theorem 1: $E^n_D=\max_{j\in[n]}E^{n,j}_D$ on $\mathcal D_{n,n}$ (p. 11).
5. Theorem 5, Csiszár's inequality: for every convex $\mathcal C\subseteq\mathcal D_n$ and $n\ge1$,

$$\mathbb P[D_{\mathrm{bs}[n]}\in\mathcal C]\le\exp\Big(-n\inf_{D\in\mathcal C}B(D,D_{\mathrm{tr}})\Big)\quad\text{(p. 14)}.$$

6. Each $\mathcal C_j=\{D\in\mathcal D^j_n:E^{n,j}_D>\bar c\}$ is convex (p. 15).
7. On $\mathcal D_{n,n}$, $E^n_D>\bar c$ if and only if $D\in\bigcup_{j}\mathcal C_j$ (p. 15).
8. $\inf_{D\in\mathcal C_j}B(D,D_{\mathrm{tr}})\ge\max\{r,r^j_n\}$ when $\bar c=\bar c_n$ (p. 15).
9. For Nadaraya–Watson, the disappointment set is convex and lies at bootstrap distance at least $r$ (B.6, p. 30).
10. Corollary 2: with $k=n$ the disappointment is at most $\exp(-n\cdot r)$ (p. 16).

Significance

Theorem 6 makes the radius $r$ an explicit statistical dial. The sum $\sum_j\exp(-n\max\{r,r^j_n\})$ can be computed from the training data, because each $r^j_n$ is a convex program. So a practitioner can choose $r$ for a target disappointment $b$, and the bound decays exponentially in $n$ at rate at least $r$. Corollary 2 gives a single exponential bound for Nadaraya–Watson: $r\ge\log(1/b)/n$ gives disappointment at most $b$. Together with the paper's Proposition 1, which shows that no smaller distance keeps the rate $-r$, the result explains why the relative entropy is the natural ambiguity measure for bootstrap guarantees.

On the formal side, the results are proved in the paper. Theorem 5 is cited there from Csiszár (1984), not reproved. The local platform search found no matching machine-checked statement of Theorem 6, Theorem 1 or Csiszár's convex-set inequality. A formal proof of Theorem 5 on a finite alphabet would be a reusable large-deviation tool: a finite-sample Sanov upper bound without polynomial prefactor, for empirical distributions of i.i.d. samples in any convex set. Theorem 1 and the partition lemma are the combinatorial facts behind the nearest-neighbours robust formulation of this paper.

Difficulty

Two steps carry the weight. The first is Theorem 5. The method of types alone gives $\mathbb P[D_{\mathrm{bs}[n]}\in\mathcal C]\le(n+1)^{|\Omega_n|}\exp(-n\inf_{\mathcal C}B)$, and its polynomial factor is fatal here: the goal has none. Removing it needs convexity of $\mathcal C$ in an essential way; the bound is false for general sets. The set $\mathcal C$ need not be closed and its infimum need not be attained. The second is Theorem 1. The estimator selects its neighbourhood depending on $D$, so it is neither linear nor concave in $D$. The disappointment event is therefore not convex, and Theorem 5 cannot be applied to it directly. Splitting it over the sets $\mathcal D^j_n$ needs the partition of $\mathcal D_{n,n}$. That partition fails off the grid $\mathcal D_{n,n}$: a mass strictly below $k/n$ is at most $(k-1)/n$ only for multiples of $1/n$.

Formalization scope

The support $\Omega_n$ is a finite type $\iota$, and a distribution is a vector ι → ℝ in stdSimplex ℝ ι. Covariates, responses, the context and the distance function of Definition 2 do not appear. The neighbourhoods are a chain N : ℕ → Finset ι with Monotone N, N 0 = ∅ and N n = univ, which abstracts Definition 2 and its tie-breaking. Weights are positive, losses are real-valued (Assumption 1 allows $+\infty$; no planned statement needs it), and nonnegativity and convexity of the loss are not assumed. The relative entropy is EReal-valued, with $0\log0=0$ and $B(D,D')=+\infty$ when $D'_i=0<D_i$. Every supremum and infimum that may be empty or unbounded is in EReal: an infeasible program (22) is $-\infty$, an empty $\mathcal D^j_n$ has $r^j_n=+\infty$, and $\exp(-n\cdot(+\infty))=0$. The bootstrap law is the product measure Measure.pi of $n$ copies of $\sum_iD_{\mathrm{tr},i}\delta_i$. The robust budget is the formulation (26), $\max_jc^j_n$, which the paper computes and which never exceeds (24). The theorem is stated for every decision $z$, not only for the robust prescriptor. The printed strict inequalities for the infima over $\mathcal C_j$ are stated as $\ge$.

Trivializing encodings are ruled out explicitly. Real sSup/sInf would turn infeasible programs and empty sets into a finite $0$. A real logarithm with a vanishing reference would give $B$ a finite junk value. A single draw or a non-product law would make Theorem 5 false. A chain without $N^0=\emptyset$ and $N^n=\Omega_n$ would break the partition. expNeg treats $+\infty$ explicitly so that an empty $\mathcal D^j_n$ contributes $0$, not $1$.

A complete development needs the method of types on a finite alphabet, I-projections onto convex sets of the simplex, and the Pythagorean inequality. The latter two are reusable well beyond this mission. Contributions to any milestone, or to a standalone finite-alphabet Csiszár inequality, are welcome.

Selected references

• D. Bertsimas and B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021. https://arxiv.org/abs/1711.09974
• I. Csiszár, Sanov property, generalized I-projection and a conditional limit theorem, Annals of Probability 12(3), 1984. https://doi.org/10.1214/aop/1176993227
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, Springer, 2nd ed., 2010. https://doi.org/10.1007/978-3-642-03311-7
• B. Efron, Bootstrap methods: another look at the jackknife, Annals of Statistics 7(1), 1979. https://doi.org/10.1214/aos/1176344552
• D. Bertsimas and N. Kallus, From predictive to prescriptive analytics, Management Science 66(3), 2020. https://doi.org/10.1287/mnsc.2018.3253

Motivation

A decision maker who chooses $x$ to minimize an expected cost $c(x,\mathbb P)=\mathbb E_{\mathbb P}[\gamma(x,\xi)]$ rarely knows the distribution $\mathbb P$ of the random parameter $\xi$. What is available is a sample $\xi_1,\dots,\xi_T$. Any rule that turns the sample into a cost estimate can disappoint: the realized expected cost may exceed the estimate. In a cost-minimization context such underestimates are more harmful than overestimates, which is why distributionally robust optimization replaces the unknown $\mathbb P$ by a worst case over a set of distributions consistent with the data.

Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118, Management Science 2021) asked which such rule is best. They define a data-driven predictor to be least conservative among all predictors whose probability of disappointment decays exponentially at a prescribed rate $r$, and they prove that a single predictor, the worst-case expected cost over a relative-entropy ball around the empirical distribution, is the unique strong solution. Their main results are for a finite set of outcomes $\Xi=\{1,\dots,d\}$. Section 5 extends the predictor result to an arbitrary compact $\Xi\subseteq\mathbb R^d$; this mission formalizes that extension. The version used throughout is the arXiv preprint arXiv:1704.04118v3 (22 December 2019), and every index below is the preprint's.

Setting

Fix compact sets $X\subseteq\mathbb R^n$ (decisions) and $\Xi\subseteq\mathbb R^d$ (outcomes), and a cost $\gamma:X\times\Xi\to\mathbb R$ that is jointly continuous.

• The model class $\mathcal P$ is the set of Borel probability distributions on $\Xi$, with the topology of weak convergence. $X\times\mathcal P$ carries the product topology.
• The model-based predictor is $c(x,\mathbb P)=\int_\Xi\gamma(x,\xi)\,\mathrm d\mathbb P(\xi)$.
• The relative entropy of $\mathbb P'$ with respect to $\mathbb P$ (Definition 8) is $I(\mathbb P',\mathbb P)=\int_\Xi\log\frac{\mathrm d\mathbb P'}{\mathrm d\mathbb P}\,\mathrm d\mathbb P'$ if $\mathbb P'\ll\mathbb P$, and $+\infty$ otherwise.
• Given independent samples $\xi_1,\dots,\xi_T$ from $\mathbb P$, the empirical distribution is $\hat{\mathbb P}_T=\frac1T\sum_{t=1}^T\delta_{\xi_t}$, and $\mathbb P^\infty$ denotes the law of the sample path.
• A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$; the estimate after $T$ samples is $\hat c(x,\hat{\mathbb P}_T)$. Its out-of-sample disappointment is $\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)$.
• Problem (5): $\hat c$ is feasible if, for all $x\in X$ and $\mathbb P\in\mathcal P$,

$$\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(x,\mathbb P)>\hat c(x,\hat{\mathbb P}_T)\big)\le -r,$$

and strongly optimal if it is feasible and $\hat c(x,\mathbb P')\le\hat c'(x,\mathbb P')$ for all $(x,\mathbb P')$ and every feasible $\hat c'$.

• The distributionally robust predictor is $\hat c_r(x,\mathbb P')=\sup\{c(x,\mathbb P):\mathbb P\in\mathcal P,\ I(\mathbb P',\mathbb P)\le r\}$.
• $\bar\gamma(x)=\max_{\xi\in\Xi}\gamma(x,\xi)$ is the worst-case cost and $\Xi^\star(x)$ the set of its maximizers.

Formalization targets

Goal: Theorem 10 (p. 26)

$$r\ge0\ \Longrightarrow\ \hat c_r\text{ is feasible in (5)},\qquad r>0\ \Longrightarrow\ \hat c_r\text{ is strongly optimal in (5)}.$$

Both halves are in the goal. The case $r=0$ of feasibility is the statement that $\hat c_0=c$ is continuous.

Milestones

• Lemma 1 (p. 23): $c$ is continuous on $X\times\mathcal P$.
• Lemma 2 (33), p. 29: $\hat c_r$ equals a supremum over pairs $(\mathbb P_c,p)$ with $\mathbb P'\ll p\,\mathbb P_c\ll\mathbb P'$, where the mass $1-p$ is placed at cost $\bar\gamma(x)$.
• Lemma 3 (p. 31): the perturbed problem (34), $\hat c_{r,\epsilon}$, satisfies $\hat c_r\le\hat c_{r,\epsilon}\le\hat c_r+\epsilon$.
• Lemma 4 (35), p. 31:

$$\hat c_{r,\epsilon}(x,\mathbb P')\le\min_{\alpha\ge\bar\gamma(x)+\epsilon}\ \alpha-e^{-r}\exp\Big(\int_\Xi\log(\alpha-\gamma(x,\xi))\,\mathrm d\mathbb P'(\xi)\Big),$$

with a minimizer $\alpha^\star\le(\bar\gamma(x)+\epsilon-e^{-r}c(x,\mathbb P'))/(1-e^{-r})$, and with equality for $\epsilon>0$.

• Proposition 6 (p. 25): $\hat c_r$ is continuous on $X\times\mathcal P$ for $r\ge0$.
• Theorem 9 (24a)/(24b), p. 25: the weak large deviation principle for $\hat{\mathbb P}_T$ in the weak topology, with the closure $\operatorname{cl}\mathcal D$ in the upper bound and the interior in the lower bound.
• (41), p. 35: if $\mathbb P_0(\Xi^\star(x))<1$ and $c(x,\mathbb P_0)\ge\hat c_r(x,\mathbb P')$, then $I(\mathbb P',\mathbb P_0)\ge r$.
• Proposition 1(ii), (iii) in the general setting (p. 24): $I$ is jointly convex and jointly lower semicontinuous on $\mathcal P\times\mathcal P$.

Proposition 5, the dual representation (23) of $\hat c_r$ itself, is included as a further item; the proof of Theorem 10 goes through Lemmas 3–4 and does not use it.

Significance

Theorem 10 says that, on any compact outcome space, no continuous predictor is less conservative than $\hat c_r$ while keeping its disappointment probability below $e^{-rT}$ to first order in the exponent. Relative-entropy distributionally robust optimization is therefore not one choice among many ambiguity sets but the optimal one for this criterion, and the dual representation turns its evaluation into a one-dimensional convex problem. The paper also shows that the continuous-state analogue of its prescriptor result (Theorem 11) only holds up to an arbitrarily small shift, so the predictor statement formalized here is the clean part of the extension.

The results are proved in the paper; none is formalized. A complete development yields a formal Sanov-type weak large deviation principle for empirical measures in the weak topology, joint convexity and lower semicontinuity of the Kullback–Leibler divergence for probability measures on a compact metric space, and a measure-theoretic dual representation of a relative-entropy worst-case expectation. Mathlib has the Kullback–Leibler divergence klDiv and the weak topology on probability measures, but none of these three results.

Difficulty

The finite-state proof of feasibility bounds the disappointment through the large deviations upper bound over the disappointment set $\mathcal D$ itself. On a continuous space that bound only holds over the closure $\operatorname{cl}\mathcal D$ in the weak topology (24a), and the paper notes that this invalidates the finite-state argument (p. 25). The rate must then be controlled on a larger, closed set of empirical distributions, where the strict inequality defining a disappointment is lost; this is where the mass that $\mathbb P_0$ puts on the worst-case scenarios $\Xi^\star(x)$ starts to matter, as the hypothesis of (41) shows.

Continuity of $\hat c_r$ in the weak topology is the second obstacle. The supremum runs over an infinite-dimensional set of distributions, a worst-case distribution may put mass outside the support of $\mathbb P'$, and the integrals involved can diverge or take the value $-\infty$. Weak convergence controls integrals of bounded continuous functions only, and $\log(\alpha-\gamma)$ is unbounded below at $\alpha=\bar\gamma(x)$.

Formalization scope

• $\mathcal P$ is ProbabilityMeasure ↥Ξ for the Borel σ-algebra of the subtype, with Mathlib's weak-convergence topology. $X$ and $\Xi$ are compact subsets of Euclidean spaces, $\gamma:↥X\to↥\Xi\to\mathbb R$ is jointly continuous; these standing assumptions of §2 (p. 5) and §5 (p. 23) appear as hypotheses of every theorem. No other hypothesis is added. Nonemptiness of $\Xi$ is automatic wherever a distribution on $\Xi$ is in scope.
• $I$ is Mathlib's InformationTheory.klDiv, valued in $[0,\infty]$. It equals Definition 8, including the value $+\infty$ when $\mathbb P'\not\ll\mathbb P$ or when the log-likelihood ratio is not integrable.
• The empirical distribution is defined for $T\ge1$. The probability of an event about $\hat{\mathbb P}_T$ is the outer measure under the product measure $\mathbb P^{\otimes T}$, and is $0$ at $T=0$; all statements are asymptotic in $T$.
• Decay rates are stated without logarithms: $\limsup\frac1T\log p_T\le-s$ becomes "for every $r'<s$, eventually $p_T\le e^{-r'T}$", which is equivalent and handles $p_T=0$. A naive Real.log encoding would be wrong, since Lean sets $\log0=0$. Predictors must be continuous for the weak topology; dropping continuity, or replacing the weak topology by a finer one, changes the problem.
• The constraint $\int\log(\frac1p\frac{\mathrm d\mathbb P'}{\mathrm d\mathbb P_c})\,\mathrm d\mathbb P'\le r$ in (33)–(34) carries an explicit integrability requirement, so that a divergent integral fails the constraint instead of evaluating to $0$. The geometric mean $\exp\int\log(\alpha-\gamma)\,\mathrm d\mathbb P'$ follows the paper's convention $\log0=-\infty$; it is defined as $\inf_{\delta>0}\exp\int\log(\alpha+\delta-\gamma)\,\mathrm d\mathbb P'$, which is the same value for $\alpha\ge\bar\gamma(x)$.
• At the end of the proof of Theorem 10 the page writes "when $\epsilon>0$" for strong optimality; the theorem statement says $r>0$, which is what is formalized.

Contributions are welcome at every level: a Sanov upper and lower bound for empirical measures on compact metric spaces, convexity and lower semicontinuity of klDiv, and the measure-theoretic duality of Lemma 4 are each reusable beyond this mission.

Selected references

• B. P. G. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From Data to Decisions: Distributionally Robust Optimization is Optimal, Management Science 67(6), 2021. Preprint arXiv:1704.04118v3. https://arxiv.org/abs/1704.04118
• I. Csiszár, A simple proof of Sanov's theorem, Bulletin of the Brazilian Mathematical Society 37(4), 2006. https://doi.org/10.1007/s00574-006-0023-1
• T. van Erven, P. Harremoës, Rényi divergence and Kullback–Leibler divergence, IEEE Transactions on Information Theory 60(7), 2014. https://doi.org/10.1109/TIT.2014.2320500
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4

Motivation

Conic optimization over the exponential cone $K_{\exp}=\operatorname{cl}\{x\in\mathbb R^3: x_1\ge x_2e^{x_3/x_2},\ x_2>0\}$ models entropy, relative entropy, logistic regression, log-sum-exp and geometric programming. Unlike the nonnegative orthant, the second-order cone and the semidefinite cone, the exponential cone is not symmetric (self-scaled), so the Nesterov–Todd primal-dual machinery that makes solvers such as SeDuMi and MOSEK fast does not apply as is. Dahl and Andersen (Math. Program. 194 (2022) 341–370) describe the nonsymmetric-cone algorithm implemented in MOSEK (version 9.2 in the paper's experiments). Its central new ingredient is a corrector for nonsymmetric cones, an analogue of Mehrotra's predictor-corrector that is responsible for much of the practical performance of symmetric-cone solvers. The paper reports that the corrector gives a substantial and consistent reduction in iteration counts across its test sets.

Timeline. Nesterov and Todd (1997, 1998) built primal-dual methods for self-scaled cones. Nesterov, Todd and Ye (1999) and Tunçel (2001) studied primal-dual scalings for general cones, Tunçel proving polynomial complexity of an infeasible method without a corrector under bounded scalings. Skajaa and Ye (2015) gave a homogeneous method for nonsymmetric cones with a Runge–Kutta corrector. Myklebust and Tunçel (2014) analysed BFGS-type scalings. Dahl and Andersen (2022) introduced the third-order corrector studied in this mission.

Setting

Let $A\colon\mathbb R^n\to\mathbb R^m$ be linear with full row rank, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and let $\hat K\subseteq\mathbb R^n$ be a proper cone (pointed, closed, convex, with nonempty interior). A $\hat\vartheta$-logarithmically homogeneous self-concordant barrier (LHSCB) for $\hat K$ is a $C^3$ convex function $\hat F$ on $\operatorname{int}\hat K$ with $|\hat F'''(x)[u,u,u]|\le2(\hat F''(x)[u,u])^{3/2}$ and $\hat F(\tau x)=\hat F(x)-\hat\vartheta\log\tau$. The primal problem minimizes $\langle c,\hat x\rangle$ subject to $A\hat x=b$, $\hat x\in\hat K$; the dual maximizes $\langle b,y\rangle$ subject to $c-A^Ty=\hat s\in\hat K^*$.

The homogeneous model adds $\tau,\kappa\ge0$: $x=(\hat x,\tau)$, $s=(\hat s,\kappa)$, $K=\hat K\times\mathbb R_+$, $F(x)=\hat F(\hat x)-\log\tau$, $\vartheta=\hat\vartheta+1$. With $z=(x,s,y)$, the residual is

$$G(z)=\bigl(A\hat x-b\tau,\ -A^Ty+c\tau-\hat s,\ b^Ty-c^T\hat x-\kappa\bigr),$$

a linear map whose $(y,\hat x,\tau)$-block is skew-symmetric. An iterate has $x\in\operatorname{int}K$, $s\in\operatorname{int}K^*$, and $\mu=\langle x,s\rangle/\vartheta$. The shadow iterates are $\tilde x=-F_*'(s)$ and $\tilde s=-F'(x)$, with $F_*$ the conjugate barrier. A scaling is a nonsingular $W$ with $v=Wx=W^{-T}s$ and $\tilde v=W\tilde x=W^{-T}\tilde s$ (the double secant equations (8)).

The affine direction $\Delta z^a$ solves $G(\Delta z^a)=-G(z)$, $W\Delta x^a+W^{-T}\Delta s^a=-v$ (11). The corrector is $\eta=-\tfrac12F'''(x)[\Delta x^a,(F''(x))^{-1}\Delta s^a]$ (16). For a centering parameter $\gamma>0$, the combined direction $\Delta z$ solves

$$G(\Delta z)=-(1-\gamma)G(z),\qquad W\Delta x+W^{-T}\Delta s=-v+\gamma\mu\tilde v-W^{-T}\eta. \tag{18}$$

Formalization targets

Goal: Lemma 4 (p. 353)

Every solution of (18) satisfies

$$\langle s,\Delta x\rangle+\langle x,\Delta s\rangle=-(1-\gamma)\langle x,s\rangle,\qquad\langle\Delta x,\Delta s\rangle=0,$$

and for all $\alpha\in\mathbb R$

$$G(z+\alpha\Delta z)=(1-\alpha(1-\gamma))G(z),\qquad\langle x+\alpha\Delta x,s+\alpha\Delta s\rangle=(1-\alpha(1-\gamma))\langle x,s\rangle.$$

The goal fixes no constants beyond those of the direction itself. It holds for every solution of (18), not a chosen one.

Milestones

1. §2 homogeneity identities (p. 345): $F'(\tau x)=F'(x)/\tau$, $F''(\tau x)=F''(x)/\tau^2$, $F''(x)x=-F'(x)$, $F'''(x)[x]=-2F''(x)$, $\langle F'(x),x\rangle=-\vartheta$.
2. §2 sum rule for the homogenizing block (pp. 345, 347): $\hat F(\hat x)-\log\tau$ is a $(\hat\vartheta+1)$-LHSCB for $\hat K\times\mathbb R_+$.
3. Lemma 2 (p. 351): the affine direction satisfies $\langle s,\Delta x^a\rangle+\langle x,\Delta s^a\rangle=-\langle x,s\rangle$, $\langle\Delta x^a,\Delta s^a\rangle=0$, and $\langle x+\alpha\Delta x^a,s+\alpha\Delta s^a\rangle=(1-\alpha)\langle x,s\rangle$.
4. Lemma 3 (p. 352): the pure corrector direction ($G(\Delta z^c)=0$, $W\Delta x^c+W^{-T}\Delta s^c=-W^{-T}\eta$) satisfies $\langle s,\Delta x^c\rangle+\langle x,\Delta s^c\rangle=0$ and $\langle\Delta x^c,\Delta s^c\rangle=0$.

Significance

The result. Lemma 4 says that a step of any length along the combined direction reduces the infeasibility residuals and the complementarity gap by exactly the same factor. Starting from a point with $\mu^0=1$, the iterates satisfy $G(z^k)=\mu^kG(z^0)$ and $\langle x^k,s^k\rangle=\mu^k\vartheta$, so the algorithm needs no merit function to balance feasibility against optimality, in contrast with earlier nonsymmetric methods. The lemma also shows that adding the third-order corrector does not cost this property, which is what justifies using the corrector in MOSEK's exponential-cone solver.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of Lemmas 2–4, the §2 homogeneity identities or the barrier sum rule has a machine-checked proof. The mission produces a formal homogeneous model for a general proper cone with a general LHSCB and a formal account of third-derivative calculus for logarithmically homogeneous barriers. Both are reusable in any analysis of interior-point methods for nonsymmetric cones (power cones, generalized power cones, hyperbolicity cones).

Difficulty

The obvious reading of Lemma 4 as bookkeeping with the linear map $G$ stalls at the corrector: the term $W^{-T}\eta$ in (18) involves the third derivative of the barrier, and nothing in linear algebra says how it interacts with the complementarity gap. Controlling it needs the third-derivative calculus of logarithmically homogeneous barriers. In Lean that means relating gradient, the Hessian as fderiv of the gradient, and the third derivative as fderiv of the Hessian, and working with the symmetry of iterated Fréchet derivatives of a $C^3$ function, for which the Mathlib interface is thin. A second obstacle is the augmented barrier: the barrier properties of $\hat F$ must be transported to $\hat F(\hat x)-\log\tau$ on $\mathbb R^{n+1}$ through the splitting $\mathbb R^{n+1}=\mathbb R^n\times\mathbb R$, including the boundary behaviour at the corner $\hat x\in\partial\hat K$, $\tau=0$.

The first identity of Lemma 4 is misprinted in the paper as $=0$. A formalization following the printed statement would be false, not merely awkward.

Formalization scope

Vectors of the augmented space are EuclideanSpace ℝ (Fin (n + 1)); $\hat x$ is the first $n$ coordinates and $\tau$ (resp. $\kappa$) the last. $A$ is a continuous linear map and $A^T$ its Hilbert adjoint; full row rank is surjectivity. Proper cones, the Hessian hess, the barrier class IsLogHomBarrier and the conjugate conj are the published SelfScaledIPM.ShortStep.Setting. That barrier class adds three standard conditions to the paper's two (boundary blow-up, the $\vartheta$-inequality and a positive definite Hessian), which the paper uses implicitly when it writes $(F''(x))^{-1}$ and calls $F$ a barrier. $W$ is a continuous linear equivalence and $W^{-T}$ the adjoint of $W^{-1}$. $F'''(x)[u,w]$ is fderiv ℝ (hess F) x u w and $(F''(x))^{-1}$ is ContinuousLinearMap.inverse. Every inner product includes the homogenizing term $\tau\kappa$.

Repairs, generalizations and specializations, each disclosed in the item statements:

• Repair: Lemma 4's first identity is stated as $-(1-\gamma)\langle x,s\rangle$, as derived in the paper's own proof, instead of the printed $0$.
• Generalization: one proper cone $\hat K$ with one barrier replaces the paper's product $K_1\times\dots\times K_k$. The product with the sum barrier is a special case.
• Generalization: $W$ is any nonsingular map satisfying (8). The paper's block-diagonal scaling with $W_{k+1}=\sqrt{\kappa/\tau}$ is a special case.
• Specialization: the sum rule is stated for $K_2=\mathbb R_+$, $F_2=-\log$, $\vartheta_2=1$, the only case the paper applies.

The directions are predicates ("$\Delta z$ solves (11)"), and the lemmas quantify over all solutions. The hypotheses are satisfiable. For the linear program $n=m=1$, $A=1$, $b=c=1$, $\hat K=\mathbb R_+$, $\hat F=-\log$, $x=s=(1,1)$, $y=0$, $W=I$, system (11) has the unique solution $\Delta x^a=(0,0)$, $\Delta s^a=(-1,-1)$, $\Delta y^a=1$. Statements that hold only because a junk value appears are ruled out: every statement requires $x\in\operatorname{int}K$ and $s\in\operatorname{int}K^*$, where $\log\tau$, the inverse Hessian and the conjugate barrier take their true values. A formalization that drops $\tau,\kappa$ from the inner products, or that fixes one solution of (18) instead of quantifying over all, would be a different lemma and does not count.

Welcome contributions: the general sum rule for products of cones, a Fin.append splitting library for EuclideanSpace, and proofs of the homogeneity identities that can be reused by the series' other missions.

Selected references

• J. Dahl, E. D. Andersen, A primal-dual interior-point algorithm for nonsymmetric exponential-cone optimization, Math. Program. 194 (2022) 341–370. https://doi.org/10.1007/s10107-021-01631-4
• Yu. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
• L. Tunçel, Generalization of primal-dual interior-point methods to convex optimization problems in conic form, Found. Comput. Math. 1 (2001) 229–254. https://doi.org/10.1007/s002080010009
• A. Skajaa, Y. Ye, A homogeneous interior-point algorithm for nonsymmetric convex conic optimization, Math. Program. 150 (2015) 391–422. https://doi.org/10.1007/s10107-014-0773-1
• T. Myklebust, L. Tunçel, Interior-point algorithms for convex optimization based on primal-dual metrics, arXiv:1411.2129 (2014). https://arxiv.org/abs/1411.2129

Motivation

In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.

Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation $RF$ of a set-partitioning formulation $F$, rather than on the LP relaxation $LF$ of that formulation. Their Theorem 2 is the justification for that design choice: the best bound $RF$ can deliver is never weaker than $z(LF)$, and can be strictly stronger. This mission formalizes that comparison.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric travel cost $d_{uv}$ (in which the fixed vehicle costs $U_1, U_2$ have already been folded into the depot–satellite and satellite–customer entries), positive integer demands $q_i$, capacities $Q_1 > Q_2 > 0$ for first- and second-level vehicles, a bound $m^1$ on first-level vehicles, $m_k$ second-level vehicles at satellite $k$, a global bound $m^2 \le \sum_k m_k$ on second-level vehicles, a capacity $B_k$ and a unit handling cost $H_k$ for each satellite.

A first-level route $r \in \mathcal M$ leaves the depot, visits a set $R_r$ of satellites and returns; its cost $g_r$ is the cost of that closed walk. A second-level route $l \in \mathcal R_k$ leaves satellite $k$, visits a set $R_{kl}$ of customers and returns; its load is $w_{kl} = \sum_{i \in R_{kl}} q_i \le Q_2$, $a_{ikl}$ counts its visits to customer $i$, and its cost $c_{kl}$ is its closed-walk cost plus $H_k w_{kl}$.

Formulation $F$ uses binaries $x_{kl}$ (route $l$ of satellite $k$ is used), binaries $y_r$, and nonnegative integers $q_{kr}$ (quantity route $r$ delivers to satellite $k \in R_r$). It minimizes $\sum c_{kl}x_{kl} + \sum g_r y_r$ subject to: each customer is covered exactly once (2); at most $m_k$ routes at satellite $k$ (3) and $m^2$ overall (4); the load delivered from satellite $k$ is at most $B_k$ (5); at most $m^1$ first-level routes (6); what first-level routes bring to satellite $k$ equals what its second-level routes carry (7); and $\sum_{k \in R_r} q_{kr} \le Q_1 y_r$ (8).

The LP relaxation $LF$ replaces the integrality of $x, y, q$ by $0 \le x, y \le 1$, $q \ge 0$. Its value is $z(LF)$, equal to $+\infty$ when $LF$ is infeasible.

The relaxation $RF(\beta, \lambda, \mu)$ relaxes (2)–(4) with penalties $\lambda \in \mathbb{R}^{N_C}$, $\mu_k \le 0$ and $\mu_0 \le 0$, and replaces the second-level routes by marginal routing costs $\beta_{ik}$ that must satisfy, for every route $l \in \mathcal R_k$,

$$\sum_{i} a_{ikl}\beta_{ik} \le c_{kl} - \sum_i a_{ikl}\lambda_i - \mu_k - \mu_0. \tag{12}$$

Its variables are binaries $\xi_{ik}$ (customer $i$ is supplied from satellite $k$), $y_r$ and $q_{kr}$; it minimizes

$$\sum_{k,i}\beta_{ik}\xi_{ik} + \sum_r g_r y_r + \sum_i \lambda_i + \sum_k m_k\mu_k + m^2\mu_0$$

subject to single assignment of each customer, flow balance $\sum_{r \in \mathcal M_k} q_{kr} = \sum_i q_i\xi_{ik}$, satellite capacity $\sum_i q_i \xi_{ik} \le B_k$, and (6), (8). A choice $(\beta,\lambda,\mu,\mu_0)$ with $\mu, \mu_0 \le 0$ and (12) is admissible.

Formalization targets

Goal: Theorem 2

$$\max_{\beta,\lambda,\mu}\, z(RF(\beta,\lambda,\mu)) \ \ge\ z(LF), \quad\text{and the inequality can be strict.}$$

Formally: (1) for every instance and route families whose $LF$ is feasible, some admissible $(\beta,\lambda,\mu,\mu_0)$ satisfies $z(LF) \le z(RF(\beta,\lambda,\mu))$; (2) some instance, route families and admissible choice give $z(LF) < z(RF(\beta,\lambda,\mu)) < +\infty$.

Milestones

• §3, remark on $LF$: if every $g_r > 0$, every optimal $LF$ solution has $y_r = (\sum_{k \in R_r} q_{kr})/Q_1$.
• Theorem 2, first clause: the bound, for every instance with $LF$ feasible.
• Theorem 2, second clause: the strict instance.

Significance

Theorem 2 places the relaxation $RF$ in the hierarchy of bounds for the 2E-CVRP. The remark on $LF$ explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so $z(LF)$ degrades as first-level routing costs grow. $RF$ keeps $y_r$ binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through $\beta$. The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation $\overline{RF}$ of the paper worth computing.

The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on $LF$ needs positive first-level route costs, and the "max" in Theorem 2 is attained only when $LF$ is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than $RF$.

Difficulty

$RF$ is not the Lagrangean dual of $F$ in the textbook sense: it changes the variables (customer-to-satellite assignments $\xi$ instead of routes $x$), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of $LF$, an admissible $\beta$ that is compatible with the flow-balance and capacity constraints of $RF$. For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, $Q_2 < Q_1$, route loads at most $Q_2$, $m^2 \le \sum_k m_k$), and $RF$ must be feasible, so that the gap is a genuine gap between finite bounds.

Formalization scope

Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families $\mathcal M$, $\mathcal R$ are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from $d$ along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, $LF$ variables real. Optimal values are infima over the feasible set in EReal, $+\infty$ for an infeasible problem; there is no junk value $0$.

Part 1 of the goal assumes $LF$ feasible: when $LF$ is infeasible the printed relation would read "$\sup = +\infty$", which is not attained by any single choice of penalties. Part 2 requires $z(RF) < +\infty$, which rules out the trivial witness of an instance with $RF$ infeasible; admissibility includes $\mu, \mu_0 \le 0$, without which the supremum is $+\infty$ for trivial reasons.

The definitions (instance, route systems, $F$, $LF$, (12), $RF$) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect $LF$ to the platform's general-form LP and its strong duality theorem are welcome.

Selected references

• R. Baldacci, A. Mingozzi, R. Roberti, R. Wolfler Calvo, An Exact Algorithm for the Two-Echelon Capacitated Vehicle Routing Problem, Operations Research 61(2), 298–314, 2013. https://doi.org/10.1287/opre.1120.1153
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 4.4, strong duality; Theorem 11.4, Lagrangean duality).

Motivation

In a time-inconsistent control problem, a control that is optimal when planned at time $t$ stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time $t$ can improve by an infinitesimal deviation on $[t,t+\varepsilon)$.

Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.

Setting

On a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$, the state $X$ is scalar ($n=1$) and the control $u$ takes values in $\mathbb R^l$:

$$dX_s=[A_sX_s+B_s'u_s+b_s]\,ds+[C_sX_s+D_su_s+\sigma_s]'\,dW_s,\qquad X_0=x_0.$$

The coefficients are deterministic functions on $[0,T]$: $A_s,b_s,Q_s\in\mathbb R$, $B_s\in\mathbb R^l$, $C_s,\sigma_s\in\mathbb R^d$, $D_s\in\mathbb R^{d\times l}$ and $R_s\in\mathbb R^{l\times l}$ symmetric. $A,B,C,D,Q,R$ are bounded, $b,\sigma$ are square integrable, $Q\ge0$, $R\succeq0$, and $G\ge0$. At time $t$, in state $x_t$, the planner evaluates

$$J(t,x_t;u)=\tfrac12\mathbb E_t\!\int_t^T\!\big(Q_sX_s^2+\langle R_su_s,u_s\rangle\big)ds+\tfrac12\mathbb E_t[GX_T^2]-\tfrac h2\big(\mathbb E_t[X_T]\big)^2-(\mu_1x_t+\mu_2)\,\mathbb E_t[X_T],$$

where $\mathbb E_t=\mathbb E[\,\cdot\mid\mathcal F_t]$. The third term (the variance-like term) and the fourth term (which depends on $x_t$) make the problem time-inconsistent. A control $u^*$ with state $X^*$ is an equilibrium (Definition 2.1) if, for every $t\in[0,T)$ and every $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}=u^*+v\mathbf 1_{[t,t+\varepsilon)}$ satisfies

$$\liminf_{\varepsilon\downarrow0}\frac{J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)}{\varepsilon}\ge0.$$

With $\Gamma^{(1)}_s=\mu_1e^{\int_s^TA_r\,dr}$, $|C|^2=C'C$ and $K=(R+MD'D)^{-1}$, the coupled Riccati system (4.9) for deterministic $(M,N)$ is

$$\begin{aligned}\dot M&=-\big[2A+|C|^2+\Gamma^{(1)}B'K(B+D'C)\big]M-Q+(B+D'C)'K(B+D'C)M^2-B'K(B+D'C)MN,& M_T&=G,\\ \dot N&=-\big[2A+\Gamma^{(1)}B'KB\big]N+B'K(B+D'C)MN-B'KBN^2,& N_T&=h.\end{aligned}$$

Given $(M,N)$, a linear ODE (4.8) determines $\Phi$ with $\Phi_T=-\mu_2$. The candidate equilibrium is the linear feedback (4.4)

$$u^*_s=\alpha_sX^*_s+\beta_s,\quad\alpha_s=-K_s\big[(M_s-N_s-\Gamma^{(1)}_s)B_s+M_sD_s'C_s\big],\quad\beta_s=-K_s(\Phi_sB_s+M_sD_s'\sigma_s).$$

Formalization targets

Goal: Theorem 4.4

Suppose $G\ge h>0$ and one of three cases holds:

• (i) $R\succeq\delta I$, $\frac{QD'D+|C|^2R}{l}+\Gamma^{(1)}\mathcal S(D'CB')\succeq0$ and $B=\lambda D'C$ with $\lambda\ge0$;
• (ii) the first two conditions of (i) and $D'D\succeq\delta I$;
• (iii) $R\equiv0$, $D'D\succeq\delta I$, $Q+\Gamma^{(1)}B'(D'D)^{-1}(B+D'C)\ge0$ and $Q+\Gamma^{(1)}B'(D'D)^{-1}D'C\ge0$.

Then

$$\text{(4.9) has a unique positive solution pair }(M,N)\text{ on }[0,T],$$

and, for every solution $\Phi$ of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.

Milestones

• Proposition 4.1: a positive solution $(M,J)$ of the transformed system (4.10) gives the positive solution $(M,M/J)$ of (4.9).
• Theorem 4.2: existence and uniqueness of positive solutions of (4.10) and (4.9) in the standard case $R\succeq\delta I$.
• Theorem 4.3: existence for (4.13) and (4.9) in the singular case $R\equiv0$.
• Three steps from the proof of Theorem 4.4:
  • $\alpha$ is bounded, so $u^*$ is admissible and $X^*$ has continuous paths with $\mathbb E\sup_s|X^*_s|^2<\infty$;
  • the ansatz $p(s;t)=M_sX^*_s-N_s\mathbb E_t[X^*_s]-\Gamma^{(1)}_sX^*_t+\Phi_s$, $k(s;t)=M_s[C_sX^*_s+D_su^*_s+\sigma_s]$ solves the adjoint flow (3.10);
  • the identity $\Lambda(s;t)=N_s[X^*_s-\mathbb E_tX^*_s]B_s+\Gamma^{(1)}_s(X^*_s-X^*_t)B_s$ holds, and $\Lambda$ satisfies condition (3.4).

Significance

The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting $h=\mu_1=0$ recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.

The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.

Difficulty

The system (4.9) is quadratic in $(M,N)$. Its solutions can blow up in finite time, and $(R+MD'D)^{-1}$ can degenerate when $M$ changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds $0<\eta\le M\le L$ and $J\ge1$, with $\eta$ and $L$ independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing $J$ directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter $t$ and the conditional expectations $\mathbb E_t[X^*_s]$ for every $s\ge t$.

Formalization scope

The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary $n$ and instantiated at $n=1$ through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, $L^2_{\mathcal F}$, Itô integrals, SDE solutions). The formalization commits to the following choices.

• Definition 2.1 uses $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence, and for every version of the state and of the perturbed states. The page writes $\lim$, which need not exist.
• The filtration is the natural, uncompleted filtration of $W$, not the augmented one.
• The state from time $t$ is encoded through the full horizon. The spike is additive on $[t,t+\varepsilon)$.
• "Essentially bounded" and "a.s., a.e." are read $d\mathbb P\otimes ds$-a.e.
• Every ODE ((4.8), (4.9), (4.10), (4.13)) is stated in integral form on $[0,T]$, because the coefficients are only bounded measurable. A solution includes invertibility of $R+MD'D$ (resp. $D'D$) on $[0,T]$. Uniqueness means agreement on $[0,T]$.
• The constants $\delta,\lambda$ are uniform in $s$, and the case conditions hold for every $s\in[0,T]$. In $\frac{QD'D+|C|^2R}{l}$, $l$ is the control dimension.
• "Let $\Phi$ be a solution of (4.8)" means every solution. "$u^*$ is an equilibrium" means that a closed-loop state exists and that the feedback is an equilibrium along every closed-loop state.
• Conditional-expectation families $\mathbb E_t[X^*_s]$ are handled through arbitrary progressive versions. Condition (3.4) is stated exactly: its first part as a localization on $\mathcal F_t$-sets, its second part with a jointly measurable version and "a.e. $s$".
• The paper's "$\beta$ uniformly bounded" is false when $\sigma$ is only square integrable. The milestone states the true claim: $\alpha$ is essentially bounded on $[0,T]$ (the coefficients are only essentially bounded) and $\beta$ is square integrable.

The goal's conclusion is Definition 2.1 itself; it does not mention $\Lambda$, $p$ or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.

Theorem 3.3 (the $n=1$ sufficient condition) is not posed here. Under the shared model it is mission I's goal at $n=1$. Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.

Selected references

• Y. Hu, H. Jin, X. Y. Zhou, Time-Inconsistent Stochastic Linear–Quadratic Control, arXiv:1111.0818v1, 2011; SIAM J. Control Optim. 50(3), 2012. https://arxiv.org/abs/1111.0818
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• S. Basak, G. Chabakauri, Dynamic mean–variance asset allocation, Review of Financial Studies 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• X. Y. Zhou, D. Li, Continuous-time mean–variance portfolio selection: a stochastic LQ framework, Applied Mathematics and Optimization 42, 2000. https://doi.org/10.1007/s002450010003
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
• Missions I and III of this series: the sufficient condition (Theorem 3.2) and the mean–variance equilibrium (Theorem 5.4).