Control Theory

Motivation

Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay $\tau$ between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of $\mathbb R^n$ with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients $\mu_1$ and $\mu_2$. They show that the system is exponentially stable when $\mu_2 < \mu_1$ (Theorems 1.1 and 1.3), and that when $\mu_2 \ge \mu_1$ stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.

• 1986–1988: Datko, Lagnese and Polis; Datko — destabilization by small delays in one-dimensional boundary-damped wave equations.
• 2006: Nicaise and Pignotti — the multi-dimensional dichotomy $\mu_2 < \mu_1$ (stability) versus $\mu_2 \ge \mu_1$ (instability for some delays), for boundary and internal feedback.

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$, split as $\Gamma = \Gamma_D \cup \Gamma_N$ with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$. Write $\nu$ for the outer unit normal and $\partial u/\partial\nu$ for the normal derivative. Let $\mu_1 > 0$, $\mu_2 > 0$ and let $\tau > 0$ be the delay. With damping coefficient $a \equiv 1$ the problem is

$$u_{tt}(x,t) - \Delta u(x,t) + \mu_1 u_t(x,t) + \mu_2 u_t(x,t-\tau) = 0 \quad \text{in } \Omega \times (0,\infty),$$ $$u = 0 \ \text{ on } \Gamma_D \times (0,\infty), \qquad \frac{\partial u}{\partial\nu} = 0 \ \text{ on } \Gamma_N \times (0,\infty),$$

with initial data $u(\cdot,0) = u_0$, $u_t(\cdot,0) = u_1$ and a history $u_t = g_0$ on $\Omega \times (-\tau, 0)$. The standard energy of a solution is

$$\mathcal E(t) = \frac12 \int_\Omega \big\{ |u_t(x,t)|^2 + |\nabla u(x,t)|^2 \big\}\,dx .$$

The condition $\mu_2 < \mu_1$ is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient $a \in L^\infty(\Omega)$ with $a \ge 0$ and $a > a_0 > 0$ near $\Gamma_N$; $a \equiv 1$ is one such coefficient.

Formalization targets

Goal: Theorem 1.4 for $a \equiv 1$

If (1.8) fails, i.e. $0 < \mu_1 \le \mu_2$, then

$$\forall \varepsilon > 0\ \exists \tau \in (0,\varepsilon)\ \exists u \text{ solving the problem with delay } \tau:\ \ \mathcal E(t) \not\to 0 \ (t \to \infty),$$

and the same holds with "$\tau \in (0,\varepsilon)$" replaced by "$\tau > M$", for every $M$. The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.

Milestones

1. (5.21)–(5.23): if $\varphi$ is an eigenfunction of the mixed Dirichlet–Neumann Laplacian, $\Delta\varphi = -\Lambda^2\varphi$, and $\lambda \in \mathbb C$ solves $\lambda^2 + (\mu_1 + \mu_2 e^{-\lambda\tau})\lambda = -\Lambda^2$, then $e^{\lambda t}\varphi(x)$ is a solution.
2. (5.24)–(5.25): with $\lambda = \alpha + i\beta$ and $\beta\tau = (2l+1)\pi$, that equation is equivalent to $\alpha^2 + \beta^2 = \Lambda^2$, $\mu_2 e^{-\alpha\tau} = 2\alpha + \mu_1$.
3. Case (a), $\mu_1 = \mu_2$: the system forces $\alpha = 0$ and $\beta^2 = \Lambda^2$.
4. Case (b), $\mu_2 > \mu_1$, (5.26)–(5.27): for every $\Lambda > 0$ and $l$ there is $\alpha \in (0, (\mu_2-\mu_1)/2)$ with $\tau(\alpha) = \alpha^{-1}\ln(\mu_2/(\mu_1+2\alpha)) > 0$ solving the system.
5. Energy of separated solutions (p. 1584): $\mathcal E(t) = e^{2\,\mathrm{Re}(\lambda)t}\,\mathcal E(0)$ with $\mathcal E(0) > 0$.
6. Delay bounds (p. 1585, corrected): $(2l+1)\pi/\Lambda < \tau < (2l+1)\pi/\sqrt{\Lambda^2 - (\mu_2-\mu_1)^2/4}$, the second when $\Lambda^2 > (\mu_2-\mu_1)^2/4$.

Significance

The result shows that the stability threshold $\mu_2 < \mu_1$ of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients $(\mu_1,\mu_2)$ for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the $a \equiv 1$ case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.

Difficulty

The scalar part is elementary. The difficulty is the spectral input. The small delays come from $\tau_{n,l} \approx (2l+1)\pi/\Lambda_n$ with $\Lambda_n \to \infty$, so the proof needs infinitely many eigenvalues $\Lambda_n^2 \to \infty$ of the Laplacian with mixed Dirichlet–Neumann conditions on a $C^2$ domain, with eigenfunctions that are $C^2$ inside and $C^1$ up to the boundary. This requires compactness of the embedding $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$, the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in $\mathbb R^n$. A single eigenpair gives only the large delays (letting $l \to \infty$); it does not give the small ones.

A second point: the paper's own bound $(2l+1)^2\pi^2/\tau_{n,l}^2 \le \Lambda_n^2$ bounds $\tau_{n,l}$ only from below, so it does not by itself give $\tau_{n,l} \to 0$; the upper bound of milestone 6 is needed.

Formalization scope

• Space: $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$. The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ ($\Omega = \{\psi < 0\}$, $\partial\Omega = \{\psi = 0\}$, $\nabla\psi \ne 0$ on $\partial\Omega$); $\nu = \nabla\psi/|\nabla\psi|$; the surface measure is pinned by the Gauss–Green formula for all $C^1$ fields.
• Solutions are complex valued functions $u(x,t)$ defined for all $t \in \mathbb R$, $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$; the equation and boundary conditions hold for $t > 0$; initial data and history are the traces of $u$. The Neumann condition uses the derivative within $\overline\Omega$. $|\nabla u|^2$ is the sum of the squared moduli of the partial derivatives.
• Corrected scope: Theorem 1.4 is printed for a general $a$ satisfying (1.17)–(1.18); §5.2 proves it only for $a \equiv 1$, which is what is stated.
• Corrected slips: (5.22) prints $\Delta\varphi = -\mu^2\varphi$ for $-\Lambda^2\varphi$; p. 1584 prints $e^{\alpha+i\beta}\varphi(x)$ for $e^{(\alpha+i\beta)t}\varphi(x)$; the p. 1585 bound is supplemented by the upper bound of milestone 6. Milestone texts are quoted verbatim, including the slips.
• The standing hypotheses (1.6)–(1.7) and the constant $\xi$ of (1.10) are not used by §5.2 and are omitted, which strengthens the statements.
• A trivializing formalization is ruled out: the goal's conclusion $\mathcal E \not\to 0$ excludes $u \equiv 0$, the energy integrand is continuous on the compact $\overline\Omega$ so the integral is genuine, and the normal derivative is taken within $\overline\Omega$ so the Neumann condition is not satisfied by a junk value.
• No statement assumes the existence of eigenvalues; supplying the spectral theory of the mixed Laplacian is part of the goal. Contributions welcome: the spectral theorem for the mixed Dirichlet–Neumann Laplacian on a bounded $C^2$ domain, boundary regularity of its eigenfunctions, and the energy identity for separated solutions.

Selected references

• S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
• R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988.
• R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986.
• P. Grisvard, Elliptic Problems in Nonsmooth Domains, Pitman, 1985 (regularity of mixed boundary value problems).

Motivation

Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback $\partial u/\partial\nu = -\mu_1 u_t$ on a part $\Gamma_N$ of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.

Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights $\mu_1$ and $\mu_2$, in any space dimension. Their Theorem 1.1 gives exponential decay when $\mu_2 < \mu_1$. This mission formalizes the converse, Theorem 1.2: when $\mu_2 \ge \mu_1$, some delays admit solutions whose energy does not decay at all.

Timeline.

• 1986: Datko, Lagnese and Polis, a one-dimensional wave equation whose delayed boundary feedback is unstable.
• 1988: Datko, instability under arbitrarily small delays for a class of hyperbolic systems.
• 2006: Xu, Yung and Li (doi:10.1051/cocv:2006021), one space dimension, by spectral analysis: stability for $\mu_2 < \mu_1$, instability for $\mu_2 > \mu_1$, possible instabilities for $\mu_1 = \mu_2$.
• 2006: Nicaise and Pignotti, the same dichotomy in any dimension $n$, with explicit destabilizing delays built from eigenfunctions (§5.1).

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$. The boundary is split as $\Gamma = \Gamma_D \cup \Gamma_N$, with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$. Write $\nu$ for the outer unit normal and $d\Gamma$ for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).

Fix $\mu_1, \mu_2 > 0$ and a delay $\tau > 0$. The problem (1.1)–(1.3) is

$$\begin{cases} u_{tt}(x,t) - \Delta u(x,t) = 0 & \text{in } \Omega \times (0,+\infty),\\ u(x,t) = 0 & \text{on } \Gamma_D \times (0,+\infty),\\ \dfrac{\partial u}{\partial\nu}(x,t) = -\mu_1 u_t(x,t) - \mu_2 u_t(x,t-\tau) & \text{on } \Gamma_N \times (0,+\infty), \end{cases}$$

with initial data $u(\cdot,0)$, $u_t(\cdot,0)$ and a history $u_t$ on $\Gamma_N \times (-\tau,0)$ (1.4)–(1.5). The standard energy of a solution is (3.7)

$$\mathcal E(t) = \frac12\int_\Omega \big(|u_t(x,t)|^2 + |\nabla u(x,t)|^2\big)\,dx .$$

Condition (1.8) of the paper is $\mu_2 < \mu_1$. This mission concerns the complementary case $\mu_2 \ge \mu_1$.

For real functions $w$ on $\Omega$, (5.11) defines $q_0(w) = \int_{\Gamma_N} |w|^2\,d\Gamma$ and $q_1(w) = \int_\Omega |\nabla w|^2\,dx$.

Formalization targets

Goal: Theorem 1.2 (p. 1563)

If $\mu_2 \ge \mu_1$, there exist delays $0 < \tau_0 < \tau_1 < \cdots$ and, for each $k$, a classical solution $u_k$ of (1.1)–(1.3) with delay $\tau_k$ and a constant $c_k > 0$ such that

$$\mathcal E_k(t) = c_k \qquad \text{for all } t \ge 0 .$$

The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.

Milestones

1. (5.1)–(5.2), pp. 1579–1580. If $\lambda \in \mathbb C$ and $\varphi$ solves $-\Delta\varphi + \lambda^2\varphi = 0$ in $\Omega$, $\varphi = 0$ on $\Gamma_D$ and $\partial\varphi/\partial\nu = -(\mu_1 + \mu_2 e^{-\lambda\tau})\lambda\varphi$ on $\Gamma_N$, then $u = e^{\lambda t}\varphi$ solves (1.1)–(1.3).
2. (5.5)–(5.7), pp. 1580 and 1582. For $b > 0$, $l \in \mathbb N$ and $b\tau = \arccos(-\mu_1/\mu_2) + 2l\pi$:

$$\cos(b\tau) = -\mu_1/\mu_2,\qquad \mu_2\sin(b\tau) = \sqrt{\mu_2^2-\mu_1^2},\qquad (\mu_1 + \mu_2e^{-ib\tau})\,ib = b\sqrt{\mu_2^2-\mu_1^2}.$$

3. Case (a), $\mu_1 = \mu_2$, p. 1581. For a normalized mixed Dirichlet–Neumann eigenfunction $\varphi$ with $-\Delta\varphi = b^2\varphi$ and $\tau = (2l+1)\pi/b$, the function $u = e^{ibt}\varphi$ is a solution and

$$\int_\Omega(|\nabla u|^2 + |u_t|^2)\,dx = 2b^2 \quad (t \ge 0).$$

4. Case (b), $\mu_2 > \mu_1$, pp. 1581–1582. A normalized minimizer $\varphi$ of $s\,q_0(w) + \sqrt{s^2q_0(w)^2 + 4q_1(w)}$, where $s = \sqrt{\mu_2^2-\mu_1^2}$, solves the variational problem (5.7) with $2b$ equal to the minimum value.

Significance

The result. Theorem 1.2 shows that the threshold $\mu_2 < \mu_1$ of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), $\tau_{n,l} = (2l+1)\pi/b_n$, become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.

The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:

• a machine-checked statement of the instability half of the paper's dichotomy;
• the reduction to a spectral problem as separate, checkable steps;
• a precise record of what the paper leaves implicit. In case (b) the existence of the minimizer is assumed ("if the minimum … is attained"), and in case (a) the existence of Dirichlet–Neumann eigenfunctions is quoted.

Difficulty

Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing $\varphi$. The goal needs a nonzero function $\varphi$ that is $C^2$ in $\Omega$ and $C^1$ up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ and of the trace into $L^2(\Gamma_N)$, followed by elliptic regularity up to a $C^2$ boundary. None of these is in Mathlib.

A shortcut does not work: in case (b) the frequency $b$ enters the boundary condition, so $\varphi$ is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by $1 + \varepsilon^2\|v\|^2$ does not literally give $g(\varepsilon) \ge g(0)$, although the first-order condition is right.

Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of $\cos(bt)\varphi$ oscillates.

Formalization scope

• Solutions are complex-valued, $u : \mathbb R^n \times \mathbb R \to \mathbb C$, as the page's $e^{\lambda t}\varphi$ with $\lambda \in \mathbb C$ are. $|u_t|^2$ and $|\nabla u|^2 = \sum_i |\partial_i u|^2$ are squared moduli.
• Classical solutions. A solution is $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$. It solves the equations for $t > 0$, and its values at $t \le 0$ are the initial data and history. The normal derivative is the derivative within $\overline\Omega$ applied to $\nu$. $C^2$ regularity up to the boundary is not required, because eigenfunctions of mixed problems generally lack it.
• The domain. The $C^2$ boundary is given by a global defining function $\psi$ with $\Omega = \{\psi < 0\}$. The surface measure is pinned down by the Gauss–Green formula for all $C^1$ vector fields, which determines it uniquely.
• Dropped hypotheses. The geometric hypotheses (1.6)–(1.7) and the parameter $\xi$ of (1.10) are not used in §5.1 and are omitted. This strengthens the statements.
• Sobolev spaces. $H^1_{\Gamma_D}(\Omega)$ is replaced in milestone 4 by the class of real functions that are $C^2$ in $\Omega$, $C^1$ on $\overline\Omega$ and zero on $\Gamma_D$, both as the minimization class and as the test class.
• Non-triviality. The goal requires the constant energy to be positive and the delays to be strictly increasing. Without positivity, the zero solution would satisfy "constant energy". Without strict monotonicity, one delay repeated would count as a sequence.

A complete development needs the following:

• Green's first identity on $C^2$ domains for functions that are $C^1$ up to the boundary;
• existence and regularity of eigenfunctions of the Laplacian with mixed boundary conditions;
• in case (b), existence of the minimizer (Rellich compactness and the trace theorem).

These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a $\varphi$ with the required properties, are welcome.

Selected references

• S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
• R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986. https://doi.org/10.1137/0324007
• R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
• G. Q. Xu, S. P. Yung, L. K. Li, Stabilization of wave systems with input delay in the boundary control, ESAIM Control Optim. Calc. Var. 12:770–785, 2006. https://doi.org/10.1051/cocv:2006021

Motivation

Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time $T>0$ chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.

Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as $t\to T$. The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).

Timeline:

• 2010: Chitour and Sigalotti (SIAM J. Control Optim. 48) prove a Lyapunov LMI for $J_n - b e_n K^T$, uniform over a bounded range $\underline b\le b\le\bar b$.
• 2017: Song, Wang, Holloway and Krstić give prescribed-time regulation with a time-varying feedback.
• 2020: Chitour, Ushirobira and Bouhemou remove the upper bound $\bar b$ (Proposition 10) and derive the prescribed-time estimate by time-varying homogeneity (Corollary 14).

Setting

Fix a positive integer $n$ and a prescribed time $T>0$. Let $(e_i)_{1\le i\le n}$ be the canonical basis of $\mathbb R^n$, and let $J_n$ be the $n$-th Jordan block, $J_n e_i = e_{i-1}$ with $e_0=0$. The perturbed chain of integrators is

$$\dot x(t) = J_n x(t) + \big(d(t) + b(t)u(t)\big) e_n, \qquad t\in[0,T),$$

with state $x(t)\in\mathbb R^n$ and control $u(t)\in\mathbb R$. Here $d$ is a measurable matched disturbance, and $b$ is an uncertain control gain with $b(t)\ge\underline b>0$ and no upper bound.

With weights $r_i = n-i+1$, the dilation is $D^{\mathbf r}_\mu = \operatorname{diag}(\mu^{r_1},\dots,\mu^{r_n})$ and $D_{\mathbf r} = \operatorname{diag}(r_1,\dots,r_n)$. An admissible weight is a continuous function $a\ge0$ on $[0,T]$ with $\int_t^T a>0$ for $t<T$. It defines

$$\lambda(t) = \frac{1}{\int_t^T a(\xi)\,d\xi},\qquad s(t) = \int_0^t\lambda(\xi)\,d\xi,\qquad 0\le t<T.$$

The parameter $\lambda$ blows up at $T$, and $s$ maps $[0,T)$ onto $[0,\infty)$. In the coordinates $y = D^{\mathbf r}_{\lambda(t)}x$ and the time $s$, the system becomes

$$y' = \big(a D_{\mathbf r} + J_n\big)y + (b u + d)e_n .$$

The feedback studied is $u = -K^T D^{\mathbf r}_\eta y$, that is $u(t) = -K^T D^{\mathbf r}_{\eta\lambda(t)}x(t)$ in the original variables, where $K\in\mathbb R^n$ and $\eta\ge1$.

Formalization targets

Goal: Corollary 14 (corrected)

There is a rate $\mu>0$ depending only on $n$ and $\underline b$ such that, for every $T$ and admissible $a$, there are $K$ and $C>0$ with

$$|x_i(t)| \le \frac{1}{(\eta\lambda(t))^{n-i+1}}\Big(C\eta\max(1,\eta^{n-1})e^{-\mu\eta s(t)}\|x(0)\| + C\max_{r\in[0,t]}|d(r)|\Big)$$

for every $\eta\ge1$, every $b\ge\underline b$, every disturbance $d$, every closed-loop solution, every $t\in[0,T)$ and every $1\le i\le n$. Since $\lambda(t)\to\infty$, every coordinate reaches $0$ at the prescribed time $T$.

Milestones

1. §3 (10): $\dot\lambda = a\lambda^2$, $\lambda$ is nondecreasing and tends to $\infty$ at $T$, and $s$ is an increasing $C^1$ bijection $[0,T)\to[0,\infty)$.
2. §3 (7)–(11): the transformed dynamics.
3. Proposition 10: $\exists\rho,S,K$ such that $(J_n - be_nK^T)^TS + S(J_n-be_nK^T)\preceq-\rho\,\mathrm{Id}$ for all $b\ge\underline b$.
4. Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$.
5. Proposition 12 (corrected): the ISS estimate (17) in the time $s$.
6. Proposition 13: the $\eta$-scaled LMI (20).

Significance

Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline $T$. The guarantee holds for every control gain $b\ge\underline b$, however large, and gives an explicit input-to-state bound for the matched disturbance. The weight $a$ is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on $b$ from the classical LMI, and is of independent use for high-gain and persistently excited systems.

On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.

Difficulty

The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, $b$ ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single $S$ and $K$ must work for all $b\ge\underline b$ at once. Second, the transformed system carries the time-varying term $a(s)D_{\mathbf r}$, and in the original time the feedback gain $\lambda(t)$ is unbounded. Estimates must survive both the rescaling by $D^{\mathbf r}_{\eta\lambda(t)}$ and the change of time. Constants that look harmless in the new time, such as the condition number of $S$ and the value $\lambda(0)$, reappear in the original variables, and dropping them makes the printed estimates false.

Formalization scope

Lean representation: vectors of $\mathbb R^n$ are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so $r_i$ = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and $e_nK^T$ is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm $\|\cdot\|$ is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every $t$ in the interval, the right-hand side is integrable on $[0,t]$ and the integral identity holds. This matches the paper's measurable $b$ and $d$. The standing assumptions are $n\ge1$ (§3), $T>0$, $a$ continuous and nonnegative on $[0,T]$ with $\int_t^Ta>0$ on $[0,T)$, and $b\ge\underline b>0$. No upper bound on $b$ is assumed anywhere. $\max|d|$ is replaced by an arbitrary bound $D$ of $|d|$ on the interval.

Corrected statements, with milestone texts kept verbatim:

• (17) as printed has no constant on the transient term and fails for $n\ge2$: with $a\equiv1$ and $y(0)=e_1$, $|y_1|$ first increases. Proposition 12 is stated with $C_S$ on that term.
• (23) as printed fails at $t=0$ whenever $\int_0^Ta<1$. The goal is stated with a constant $C$ on the transient term, and $K$ and $C$ may depend on $T$ and $a$. The rate $\mu$ and the disturbance gain $C_S$ depend only on $n$ and $\underline b$, as on the page.
• Proposition 13's undefined $\mu_*$ is the $\rho$ of its statement.
• "$\lambda$ increasing" is read as nondecreasing.
• Corollary 14's "$t\ge0$" is read as $t\in[0,T)$.

Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to $0$. Every constant is quantified before the objects it must not depend on: the rate $\mu$ before $T$ and $a$, $K$ before $\eta$, and $\rho,S,K$ before $b$. No statement weakens the estimates to mere convergence.

Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.

Selected references

• Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2):1022–1048, 2020. https://doi.org/10.1137/19M1285937
• Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83:243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
• Y. Chitour, M. Sigalotti, On the stabilization of persistently excited linear systems, SIAM J. Control Optim. 48:4032–4055, 2010. https://doi.org/10.1137/080737812

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

Service systems such as public fast-charging stations for electric vehicles let each customer choose how long to be served. Lin, Shang and Sun (SSRN 3709573, 2020; later in Management Science, doi:10.1287/mnsc.2022.4474) study a firm that announces to every arriving customer the current wait time $w$ (the work already in the queue) and a price rate $p$ per unit of service time. The customer then decides whether to join and, if so, how long a service to buy. Queue pricing usually conditions on the queue length with random service times (Low 1974; Paschalidis and Tsitsiklis 2000; Kim and Randhawa 2018). Here the state is the wait time, and it moves deterministically between arrivals.

The firm maximizes long-run average revenue or social welfare. The optimality condition the paper derives is not an ordinary differential equation but a delay differential equation (DDE) that looks ahead: the value at $w$ depends on the value at $w + \mathtt t(p) > w$. This mission formalizes the paper's existence theorem for that equation.

Setting

A model has a usage utility $U$, a waiting cost $c$, a Poisson arrival rate $\lambda > 0$ and a maximum service time $C > 0$, under Assumption 1 (p. 7):

1. $U(t) \ge 0$, $U(0) = 0$, $0 \le U'(t) \le U'(0)$ and $U''(t) < 0$ on $[0, C]$;
2. $\frac{d^2}{dt^2}[U'(t)t] < 0$ on $[0, C]$;
3. $c(0) = 0$, $c'(w) > 0$ and $c''(w) \ge 0$ for $w \ge 0$.

At price $p \in [0, U'(0)]$ a joining customer chooses the service time $\mathtt t(p) = \min\{(U')^{-1}(p), C\}$ (5). They join when $U(\mathtt t(p)) - p\,\mathtt t(p) - c(w) \ge 0$. Three thresholds follow:

• $\bar w$ solves $U(C) = c(\bar w)$; above it nobody joins.
• $\Gamma(w)$, for $w \in [0, \bar w]$, is the highest price at which a customer still joins (Proposition 2).
• $\hat w$ and $L(w)$ (Proposition 1) describe when the marginal price $U'(t)$ still attracts a customer.

The per-customer value is $\mathbf v(p) - \alpha c(w)$, with $\mathbf v(p) = p\,\mathtt t(p)$, $\alpha = 0$ for revenue and $\mathbf v(p) = U(\mathtt t(p))$, $\alpha = 1$ for welfare (Lemma 1).

The optimality equations (12)–(15) ask for a constant $\mathsf g$ (the average rate) and a relative value function $V$ with

$$\mathsf g = -V'(w) + \lambda \max\Big\{\max_{p \in [0, \Gamma(w)]} \big[\mathbf v(p) - \alpha c(w) + V(w + \mathtt t(p)) - V(w)\big],\ 0\Big\}, \quad w \in (0, \bar w],$$ $$\mathsf g = \lambda \max\Big\{\max_{p \in [0, \Gamma(0)]} \big[\mathbf v(p) + V(\mathtt t(p)) - V(0)\big],\ 0\Big\}, \qquad \mathsf g = -V'(w) \ (w > \bar w), \qquad V(\bar w) = 0.$$

Algorithm 1 (p. 14) is a backward explicit-Euler shooting scheme. For a guess $g \ge 0$ and $N$ grid cells on $[0, \bar w]$, it starts from $V^g_N(w) = -(w - \bar w)g$ for $w \ge \bar w$. It then builds a piecewise-linear $V^g_N$ cell by cell from right to left. On the cell ending at $x$ the slope is $-g + K^g_N(x)$, where the slope adjustment $K^g_N(x)$ is $\lambda$ times the positive part of the inner maximum at $x$. The shooting value is $g_N = \min\{g \ge 0 : g \ge K^g_N(0)\}$ (23). Finally $\bar g = \lim_j g_{2^j}$ (24) and $V^{\bar g}(w) = \lim_j V^{\bar g}_{2^j}(w)$ (Proposition 6).

Formalization targets

Goal: Theorem 1 (p. 17)

$$\bar g = \lim_{j\to\infty} g_{2^j} \ \text{exists},\quad V^{\bar g}_{2^j}(w) \to V^{\bar g}(w)\ (w \ge 0),\quad (\bar g, V^{\bar g}) \text{ solves (12)–(15)},\quad V^{\bar g} \text{ is nonincreasing and concave on } [0, \bar w + C].$$

Milestones

The milestones follow the paper's proof in order:

• Thresholds and the value function (Propositions 1–3, pp. 8–11): uniqueness of $\hat w$ and $\bar w$, the characterization (8) of $\Gamma$, $\Gamma(0) = U'(0)$ with $\Gamma$ decreasing, and the bounds (V1)–(V2) on $\mathbf v$.
• The finite-$N$ scheme (Proposition 4, Lemmas 2, 3, 5): $V^g_N$ is concave and $K^g_N$ is nonincreasing; $K$ increases when the grid is refined and decreases in $g$; and $K^{U'(0)}_N \equiv 0$.
• The limits (Proposition 5, Lemma 6, Proposition 6): $g_{2^j}$ increases to $\bar g \le U'(0)$, the $V^{\bar g}_{2^j}$ are uniformly $\bar g$-Lipschitz, and they converge uniformly to a concave, nonincreasing, Lipschitz $V^{\bar g}$.
• The equations in the limit (Lemma 7, Propositions 7–8): $K^{\bar g}_{2^j}(0) \to \bar g$; the boundary condition (13); differentiability of $V^{\bar g}$ on $[0, \bar w]$ and the DDE (12).

Significance

Theorem 1 is the existence half of the paper's verification argument. Its Theorem 2 then shows that the constructed $\bar g$ equals the optimal long-run average rate over all predictable price processes. Its Theorem 3 reads the structure of the optimal price and service-time policies off $V^{\bar g}$. Without a solution of (12)–(15) neither result has an object to talk about. The construction also gives a convergent numerical method (Algorithm 1) for a class of look-ahead DDEs that standard ODE theory does not cover.

The proofs are written out in the paper's Appendix B, except Lemma 12, an internal step of Proposition 8 whose proof the authors leave out. None of it is machine-checked. A complete formalization would check every step of the shooting argument and supply the omitted lemma. It would also yield a reusable framework: Euler-type schemes for delay equations whose delay points forward, monotone in the grid and in a scalar parameter.

Difficulty

The obvious approach, Cauchy–Lipschitz, fails: (12) is not an initial-value problem. $V'(w)$ depends on $V$ on $[w, w + C]$, so the equation must be integrated backwards from $\bar w$, and then the value $\mathsf g$ is unknown. The shooting scheme fixes $g$, integrates backwards, and tunes $g$ so that the boundary condition (13) at $w = 0$ holds in the limit. For fixed $g$ the approximations need not converge as $N \to \infty$ (the slope at $0$ can diverge), so $g$ and $N$ must be coupled through $g_N$.

The hard step is Proposition 8. Each $V^{\bar g}_{2^j}$ has kinks at every grid point, yet the limit has to be differentiable. One has to show that the left and right derivatives of the concave limit coincide and equal the right-hand side of (12), which requires passing a maximum over a $w$-dependent price set to the limit.

Formalization scope

All declarations live in the namespace WaitTimePricing.Existence, and only Mathlib is imported. Conventions:

• $U, c : \mathbb R \to \mathbb R$ are $C^3$ and $C^2$ on $\mathbb R$, a disclosed strengthening of "three/two times differentiable". Assumption 1's inequalities are imposed exactly on $[0, C]$ and $[0, \infty)$. $\lambda > 0$ and $C > 0$ are added; the paper uses them without stating them.
• $\mathtt t(p) = \sup\{t \in [0, C] : p \le U'(t)\}$, meaningful for $p \in [0, U'(0)]$. $\hat w$, $L(w)$, $\bar w$ and $\Gamma(w)$ are defined by their characterizing sets, not by closed forms. Propositions 1–2 are theorems about these sets.
• The objective is one of Lemma 1's two cases. The paper's remark that any $\mathbf v$ satisfying (V1)–(V2) would do is not formalized, because it silently needs continuity of $\mathbf v$.
• Every "max" in (12), (13), (19) and (22) is a real supremum over $[0, \Gamma(w)]$. For the continuous $V$ used here this set is nonempty and bounded, and the supremum is attained.
• $V'$ is never a default-valued derivative. (12) and (14) assert that $V$ has the prescribed derivative, two-sided for $w \in (0, \bar w]$ and $w > \bar w$; Proposition 8 states the case $w = 0$ with a right derivative.
• Algorithm 1 is a recursion over the passes of its loop, with $N \ge 1$. The initialization (16) is extended from $[\bar w, \bar w + C]$ to $[\bar w, \infty)$ so that (14) can hold as printed on $(\bar w, \infty)$. Only values on $[0, \bar w + C]$ enter the loop, so the construction is unchanged.
• $\bar g$ and $V^{\bar g}$ are defined as limits that take a default value when the limit does not exist. Propositions 5–6 and the goal assert the convergence.
• "Decreasing" is nonincreasing everywhere (including $\Gamma$, Proposition 2(iii)), the reading the proofs establish.

Trivializations ruled out. The goal names the paper's $\bar g$ and $V^{\bar g}$ together with their convergence, not an arbitrary solution and not default values of undefined limits. It cannot be met at a kink through a default-valued derivative. Its inner maxima cannot vanish through an empty or unbounded set. $\Gamma$ and $\mathtt t$ are not closed forms that would make (8) true by definition. The weaker statement "some $(\mathsf g, V)$ solves (12)–(15)" is not the goal.

Contributions are welcome at every milestone. Reusable pieces include monotonicity of a max-operator under backward induction, Dini-type uniform convergence of monotone sequences of equi-Lipschitz concave functions, and the differentiability of a concave limit of piecewise-linear functions. Theorem 2 (optimality over predictable controls) and Theorem 3 (policy structure) are outside this mission. Theorem 3 appears to fail as printed when $\bar g > U'(C)$.

Selected references

• C.-A. Lin, K. Shang, P. Sun, Wait Time Based Pricing for Queues with Customer-Chosen Service Times, SSRN 3709573, version of October 12, 2020. https://ssrn.com/abstract=3709573 (journal version: Management Science, https://doi.org/10.1287/mnsc.2022.4474)
• D. W. Low, Optimal dynamic pricing policies for an M/M/s queue, Operations Research 22(3), 1974. https://doi.org/10.1287/opre.22.3.545
• I. C. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842140
• J. Kim, R. S. Randhawa, The value of dynamic pricing in large queueing systems, Operations Research 66(2), 2018. https://doi.org/10.1287/opre.2017.1668
• D. P. Bertsekas, Dynamic Programming and Optimal Control, 2nd ed., Athena Scientific, 2000. http://www.athenasc.com/dpbook.html