Control Theory

Motivation

Boundary feedback stabilization of the wave equation asks whether a vibrating body at rest on part of its boundary can be brought to rest by a damping law on the rest of its boundary. With the undelayed velocity feedback $\partial u/\partial\nu = -\mu_1 u_t$, the energy decays exponentially under geometric conditions on the domain; results of this kind go back to Chen (1979, 1981), Lagnese (1983, 1988), Lasiecka and Triggiani (1987), and Komornik and Zuazua (1990).

Real controllers act with a delay, and delays can destroy stability. Datko, Lagnese and Polis (1986) and Datko (1988) showed that an arbitrarily small delay in a boundary feedback that stabilizes the one-dimensional wave equation can make the closed loop unstable. For a feedback made of an undelayed part and a delayed part, $\mu_1 u_t(t) + \mu_2 u_t(t-\tau)$, Xu, Yung and Li (2006) proved, by spectral analysis in one space dimension, that the system is stable when $\mu_2 < \mu_1$. Nicaise and Pignotti (2006) extended the stability result to bounded domains in any dimension $n$. This mission formalizes that extension: Theorem 1.1 of their paper.

Setting

Let $\Omega \subset \mathbb R^n$ ($n \ge 1$) be a bounded open set whose boundary $\Gamma$ is 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 \ne \emptyset$. Let $\nu$ be the outer unit normal and $d\Gamma$ the surface measure on $\Gamma$. Fix the undelayed gain $\mu_1 > 0$, the delayed gain $\mu_2 > 0$ and the delay $\tau > 0$. The problem is

$$\begin{aligned} u_{tt} - \Delta u &= 0 && \text{in } \Omega \times (0,\infty), &(1.1)\\ u &= 0 && \text{on } \Gamma_D \times (0,\infty), &(1.2)\\ \tfrac{\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), &(1.3) \end{aligned}$$

with initial data $u(\cdot,0) = u_0$ and $u_t(\cdot,0) = u_1$ in $\Omega$, and a history $u_t = f_0$ on $\Gamma_N \times (-\tau, 0)$ (1.4)–(1.5).

The geometric hypothesis requires a function $v \in C^2(\overline\Omega)$ and a constant $\alpha > 0$ with two properties:

$$\langle D^2 v(x)\xi,\xi\rangle \ge 2\alpha|\xi|^2 \quad (x \in \overline\Omega,\ \xi \in \mathbb R^n), \tag{1.6}$$ $$\nabla v(x)\cdot\nu(x) \le 0 \quad (x \in \Gamma_D). \tag{1.7}$$

For example, $v(x) = |x|^2$ satisfies both on an annulus whose inner sphere is $\Gamma_D$.

Assume the gain condition

$$\mu_2 < \mu_1, \tag{1.8}$$

and fix $\xi$ with

$$\tau\mu_2 < \xi < \tau(2\mu_1 - \mu_2). \tag{1.10}$$

The energy of a solution is the standard wave energy plus a term that stores the delayed velocity:

$$E(t) = \frac12\int_\Omega \{u_t^2(x,t) + |\nabla u(x,t)|^2\}\,dx + \frac{\xi}{2}\int_{\Gamma_N}\int_0^1 u_t^2(x,t-\tau\rho)\,d\rho\,d\Gamma. \tag{1.9}$$

Formalization targets

Goal: Theorem 1.1 (exponential decay)

There are constants $C_1, C_2 > 0$, depending on $\Omega, \Gamma_D, \Gamma_N, v, \alpha, \mu_1, \mu_2, \tau, \xi$ but not on the solution, such that every regular solution satisfies

$$E(t) \le C_1 E(0)\, e^{-C_2 t} \qquad \forall t \ge 0. \tag{1.11}$$

The constants are existential and are not fixed numerically. Any valid pair proves the goal.

Milestones, in the order the paper's proof uses them

1. (3.6): the energy identity, which expresses $E'(t)$ through boundary integrals over $\Gamma_N$ only.
2. Proposition 3.1: $E$ is nonincreasing, and

$$E'(t) \le -C\int_{\Gamma_N}\{u_t^2(x,t) + u_t^2(x,t-\tau)\}\,d\Gamma, \qquad C = \min\Big\{\mu_1 - \frac{\mu_2}{2} - \frac{\xi}{2\tau},\ -\frac{\mu_2}{2} + \frac{\xi}{2\tau}\Big\} > 0.$$

3. (3.22): the integrated form $E(T) - E(0) \le -C\int_0^T\int_{\Gamma_N}\{u_t^2(t) + u_t^2(t-\tau)\}\,d\Gamma\,dt$.
4. Proposition 3.2 (observability): there is $\overline T > 0$ such that for every $T > \overline T$ some $C_0 > 0$ satisfies

$$E(0) \le C_0\int_0^T\int_{\Gamma_N}\{u_t^2(x,t) + u_t^2(x,t-\tau)\}\,d\Gamma\,dt. \tag{3.10}$$

5. Contraction: there are $T > 0$ and $0 \le \tilde C < 1$ with $E(T) \le \tilde C E(0)$ for every regular solution.

Significance

The theorem shows that adding a delayed component to a stabilizing boundary feedback preserves exponential decay if the delayed gain is dominated by the undelayed gain. It holds in every dimension, under the same geometric condition that governs the undelayed problem. The companion Theorem 1.2 of the same paper shows that the condition $\mu_2 < \mu_1$ cannot be removed: when it fails, there are delays for which some solutions keep constant, positive standard energy. The Lyapunov functional (1.9) became a standard device for delayed feedbacks in later work on wave, plate and Timoshenko systems.

The result was proved in 2006. It has no machine-checked proof. This mission produces:

• a formal statement of the theorem on classical solutions;
• the energy identity and dissipation inequality with explicit constants;
• the observability inequality as a separate target, which is the deep analytic input and is reusable by any stabilization argument on the same geometry.

Difficulty

The dissipation inequality (Proposition 3.1) is a calculation: Green's formula, a change of variables in the delay variable $\rho$, and Young's inequality. The difficulty is entirely in the observability inequality (3.10). The obvious multiplier argument, which multiplies the equation by $\nabla v\cdot\nabla u$ and integrates, leaves a lower-order term $\|u\|$ that the boundary observation does not control.

The paper removes that term in two steps. The first is a Carleman-type estimate of Lasiecka, Triggiani and Yao (1999), which is where hypotheses (1.6)–(1.7) enter. The second is a compactness–uniqueness argument closed by Holmgren's uniqueness theorem. None of these tools exists in Mathlib, and neither does Green's formula on a curved domain. The final step from a one-period contraction to exponential decay uses time-translation invariance and monotonicity of $E$.

Formalization scope

• Domain. A MixedDomain n bundles the following:

  • a bounded open set given by a global $C^2$ defining function $\psi$ ($\Omega = \{\psi < 0\}$, $\partial\Omega = \{\psi = 0\}$, $\nabla\psi \ne 0$ on $\partial\Omega$);
  • the split $\Gamma_D \cup \Gamma_N = \partial\Omega$ with disjoint closures and $\Gamma_D \ne \emptyset$;
  • a finite measure $\sigma$ carried by $\partial\Omega$ satisfying the Gauss–Green formula for every $C^1$ vector field.

  The outer normal is $\nu = \nabla\psi/|\nabla\psi|$. The Gauss–Green requirement determines $\sigma$ uniquely as the surface measure, so the normalization of $d\Gamma$ in (1.9) and (1.10) is the paper's.

• Solutions are real-valued and classical: $u$ is one $C^2$ function on $\mathbb R^n \times \mathbb R$. It satisfies (1.1)–(1.3) for $t > 0$, and its values at $t \le 0$ are the initial data and the history. Time derivatives are one-variable derivatives in $t$, and $\partial u/\partial\nu = \nabla u \cdot \nu$. This is a subclass of the paper's solutions, so the formal theorems are the paper's restricted to smooth, compatible data.

• Added hypothesis. In Proposition 3.2, the contraction step and the goal, every connected component of $\Omega$ has a boundary point in $\Gamma_D$ (true whenever $\Omega$ is connected). The paper's uniqueness step ("$-\Delta w = 0$, $w = 0$ on $\Gamma_D$, $\partial w/\partial\nu = 0$ on $\Gamma_N$, so $w \equiv 0$") needs every component of $\Omega$ to meet $\Gamma_D$.

• Strengthened statements. The identity (3.6) and Propositions 3.1 and (3.22) omit hypotheses they do not use. Proposition 3.1 states the explicit constant $C$ from the end of its proof.

• Conventions. Condition (1.10) is strict. The energy is $E$ of (1.9), with the delay term, and not the standard energy. Derivatives of $E$ are asserted with HasDerivAt.

• Excluded trivializations. Three things would make the statements empty or different, and none of them is allowed:

  • a free measure in place of the surface measure;
  • the standard energy in place of $E$;
  • replacing (1.11) by $E(t) \to 0$.

  The degenerate case $\Gamma_N = \emptyset$ is already excluded by (1.6), (1.7) and Gauss–Green together.

• Infrastructure needed and welcome:

  • Gauss–Green and Green's first identity on MixedDomain;
  • differentiation under the integral over $\Omega$ and $\Gamma_N$;
  • a Carleman or multiplier observability estimate for the wave equation with mixed boundary conditions;
  • unique continuation (Holmgren) for the wave equation;
  • the elementary lemma turning a one-period contraction plus monotonicity into exponential decay.

  The last lemma and Gauss–Green on $C^2$ domains are reusable far beyond this mission.

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) (2006), 1561–1585. https://doi.org/10.1137/060648891
• 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 (2006), 770–785. https://doi.org/10.1051/cocv:2006021
• 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 (1986), 152–156. 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 (1988), 697–713. https://doi.org/10.1137/0326040
• I. Lasiecka, R. Triggiani, P. F. Yao, Inverse/observability estimates for second-order hyperbolic equations with variable coefficients, J. Math. Anal. Appl. 235 (1999), 13–57. https://doi.org/10.1006/jmaa.1999.6348
• V. Komornik, E. Zuazua, A direct method for the boundary stabilization of the wave equation, J. Math. Pures Appl. 69 (1990), 33–54.
• J. Lagnese, Decay of solutions of wave equations in a bounded region with boundary dissipation, J. Differential Equations 50 (1983), 163–182. https://doi.org/10.1016/0022-0396(83)90073-6

Motivation

Many control tasks come with a deadline: a consensus protocol or a regulation task must reach its target by a time fixed in advance, whatever the initial condition. Prescribed-time stabilization asks for a feedback law that brings every trajectory of a control system to the equilibrium by a user-chosen time $T$. The basic test case is the chain of integrators $x_1^{(n)}=u$, the normal form of every single-input feedback-linearizable system.

Two routes to prescribed-time stabilization exist. Time-varying gains that blow up as $t\to T$ (Song, Wang, Holloway and Krstić, Automatica 2017) are fragile under measurement noise. Fixed-time stabilization gives a settling time bounded uniformly over all initial conditions, and a time rescaling then turns the uniform bound into any prescribed $T$. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) follow the second route with an explicit, continuous feedback. It combines Hong's backstepping homogeneous controller (Systems Control Lett. 2002) with a degree of homogeneity that depends on the state (Harmouche, Laghrouche, Chitour and Hamerlain, Int. J. Control 2017). A continuity device of Lopez-Ramirez, Efimov, Polyakov and Perruquetti (Int. J. Robust Nonlinear Control 2018) makes that degree a continuous function of the state. This mission formalizes the construction and its main results, §4.1–4.2 of the paper.

Setting

Fix $n\ge1$ and write $x=(x_1,\dots,x_n)\in\mathbb R^n$ with the Euclidean norm. Let $J_n$ be the $n$-th Jordan block ($J_ne_i=e_{i-1}$, $e_0=0$). The pure chain of integrators (31) is

$$\dot x=J_nx+u\,e_n .$$

For $y\in\mathbb R$ and $a>0$ write $\lceil y\rfloor^a=\operatorname{sign}(y)|y|^a$. Given gains $\ell_1,\dots,\ell_n>0$ and $\kappa\in[-\tfrac1{2n},\tfrac1{2n}]$, set $r_j=1+(j-1)\kappa$ and $\beta_j=(2+\kappa)/r_{j+1}-1$. Define $v_0=0$ and

$$v_j=-\ell_j\Big\lceil\lceil x_j\rfloor^{\beta_{j-1}}-\lceil v_{j-1}\rfloor^{\beta_{j-1}}\Big\rfloor^{\frac{r_j+\kappa}{r_j\beta_{j-1}}} .$$

The homogeneous feedback is $\omega^H_\kappa(x)=v_n(x)$ (Definition 23). The associated Lyapunov function is

$$V_\kappa(x)=\sum_{j=1}^n\frac{|x_j|^{\beta_{j-1}+1}-|v_{j-1}|^{\beta_{j-1}+1}}{\beta_{j-1}+1}-\lceil v_{j-1}\rfloor^{\beta_{j-1}}(x_j-v_{j-1}),$$

and (36) is the decay inequality $\dot V_\kappa\le-CV_\kappa^{1+\alpha(\kappa)}$, with $\alpha(\kappa)=\kappa/(2+\kappa)$ and one constant $C$ for all $\kappa$ in the range.

For $m\in(0,1)$ and $\kappa_0\in(0,\tfrac1{2n})$, the state-dependent degree $\kappa(x)$ of (49) equals $\kappa_0$ where $V_0(x)>1+m$ and $-\kappa_0$ where $V_0(x)<1-m$, and it interpolates linearly in $V_0$ in between. The closed-loop controller is $\omega^H_{\kappa(x)}(x)$. With $B^\kappa_{<a}=\{V_\kappa<a\}$, let $r(m,\kappa_0)$ be the largest $r$ with $B^{\kappa_0}_{<r}\subseteq B^0_{<1+m}$, and $r(m,-\kappa_0)$ the smallest $r$ with $B^{-\kappa_0}_{<r}\supseteq B^0_{<1-m}$. Set

$$T^\ast(m,\kappa_0)=\frac1C\Big(\frac{r(m,\kappa_0)^{-\alpha(\kappa_0)}}{\alpha(\kappa_0)}-2\ln(2m)+\frac{r(m,-\kappa_0)^{-\alpha(-\kappa_0)}}{-\alpha(-\kappa_0)}\Big).$$

Finally $D^{\mathbf r}_\lambda=\operatorname{diag}(\lambda^{n-i+1})$ is the dilation of (5).

A system is globally fixed-time stable with settling time at most $T$ if the origin is an equilibrium, solutions exist from every initial state, it is Lyapunov stable, and every solution vanishes for all $t\ge T$ (Definition 1 with $\Omega=\mathbb R^n$).

Formalization targets

Goal: Theorem 30 (p. 1038)

Let the gains and $C>0$ satisfy (36). There are $m\in(0,1)$ and $\kappa_0\in(0,\tfrac1{2n})$ such that, for every $T>0$ and every $\lambda>0$ with

$$\lambda\ \ge\ T^\ast(m,\kappa_0)/T,$$

the feedback $u=\omega^H_{\kappa(D^{\mathbf r}_\lambda x)}(D^{\mathbf r}_\lambda x)$ makes (31) globally fixed-time stable with settling time at most $T$.

Milestones

• Proposition 24 (p. 1034): gains exist for which (36) holds uniformly in $\kappa$, $V_\kappa$ is $C^1$, positive definite and $\mathbf r(\kappa)$-homogeneous of degree $2+\kappa$, and $\omega^H_\kappa$ is globally asymptotically stabilizing.
• Lemma 31 (p. 1038): on the shell $B^\kappa_{1-m,1+m}$, $|x_j|$ and $|v_j|$ are bounded uniformly in $\kappa$.
• Lemma 32 (p. 1039): on that shell, $|\omega^H_\kappa-\omega^H_0|$ and $|V_\kappa-V_0|$ are at most a constant times $|\kappa|^{\min(1,r_n)}$.
• Proposition 33 (p. 1040): for every $m$ there is $\kappa_0(m)>0$ below which the closed loop is fixed-time stable, with an explicit settling-time bound that coincides with (52) for $m\le(\sqrt{17}-3)/4$.
• Theorem 28 (pp. 1036–1037): with an input gain $b(t)\in[\underline b,\bar b]$ and the feedback $\omega^H_{\kappa(x)}(x)/\underline b$, the closed loop is globally fixed-time stable with settling time at most $T^\ast(m,\kappa_0)$.

Significance

The result gives a static, continuous state feedback for the chain of integrators with an explicit settling-time bound. It is robust to a bounded uncertain input gain, and the rescaled controller meets any prescribed deadline. Unlike time-varying designs, the gains stay bounded, which is what the paper's ISS analysis in §4.3 builds on. The constants in (52) are explicit in terms of $C$ and the radii $r(m,\pm\kappa_0)$, so the rescaling factor $\lambda$ is computable.

The results are proved on paper; no machine-checked proof is known. A formalization would check the parameter bookkeeping of the construction: index shifts, exponents, the three-phase settling-time estimate, and the interplay of two different dilations. It would also produce reusable definitions of Carathéodory solutions and of finite-, fixed- and prescribed-time stability, which the platform does not yet have.

Difficulty

The obvious argument uses the Lyapunov function $V_{\kappa(x)}$ for the varying-degree controller. That fails: $\kappa$ depends on $x$, so $V_{\kappa(x)}(x)$ acquires a term from the derivative of $\kappa$. The proof instead handles three regions separately, with $V_{\kappa_0}$ outside $B^0_{1+m}$, $V_0$ on the shell $B^0_{1-m,1+m}$, and $V_{-\kappa_0}$ inside $B^0_{1-m}$. On the shell the controller is a perturbation of the linear one, and bounding that perturbation needs uniform Hölder estimates in $\kappa$ (Lemmas 31–32). The closed loop is only continuous, so solutions need not be unique and every stability claim is about all solutions. Proposition 24 itself is a recursive gain construction whose constants must be uniform in $\kappa$.

Formalization scope

States are EuclideanSpace ℝ (Fin n); the paper's index $j\in\{1,\dots,n\}$ is j.val + 1. Solutions are Carathéodory solutions on $[0,\infty)$ in integral form, with integrability stated. Every stability property quantifies over all solutions, and existence of a solution from each initial state is part of Lyapunov stability. $\lceil y\rfloor^a$ is read as $\operatorname{sign}(y)|y|^a$; the paper never defines it. $\dot V$ is the Fréchet derivative applied to the vector field. $r(m,\kappa_0)$ and $r(m,-\kappa_0)$ are the supremum and infimum of the admissible radii.

Hypotheses and readings that differ from the page:

• The gains and $C$ in Theorems 28 and 30 and Proposition 33 are data satisfying (36), not existentially chosen. An unconstrained $\exists C$ would make (52) false, and Proposition 24 shows (36) is satisfiable.
• $b$ is assumed measurable in Theorem 28.
• "Adapted" is the feedback divided by $\underline b$, as the page says.
• Corrected printed slips:
  • (51) lacks $e_n$.
  • Theorem 30 writes $\kappa_0\in(0,1/n)$; Theorem 28's $(0,\tfrac1{2n})$ is used.
  • Proposition 33 prints $\kappa_0(m)\in[-\tfrac1{2n},-\tfrac1{2n}]$; the value is positive and at most $\tfrac1{2n}$.
  • (37) prints $\beta_{i-1}$ for $\beta_{j-1}$.
  • The proof of Lemma 32 prints the exponent of (33) as $(r_j+1)/(r_j\beta_{j-1})$; (33) is used.
• Lemma 32's maxima are read pointwise, with $r_n=r_n(\kappa)$.
• In Proposition 33 the middle term $-2\ln(2m)$ of (52) is replaced by $\max(-2\ln(2m),\,2\ln\frac{1+m}{1-m})$: the page's crossing-time estimate $-2\ln(2m)/C$ is justified only for $m\le(\sqrt{17}-3)/4$, where the two bounds coincide.
• "Explicit" constants are stated as existing.

A formalization in which (36) is dropped, or $C$ is chosen freely, or a trajectory is only required to exist, would be trivial or false. Any trivializing reading of this kind is ruled out: stability is required of every solution, and $C$ is tied to (36).

Needed infrastructure: signed powers and their Hölder estimates (42), differentiability of $V_\kappa$, weighted homogeneity, Carathéodory existence for continuous right-hand sides, and comparison lemmas for $\dot V\le-cV^{1+\alpha}$. The stability definitions and the comparison lemmas are reusable beyond this mission. Contributions of any of these are welcome.

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. Hong, Finite-time stabilization and stabilizability of a class of controllable systems, Systems Control Lett. 46, 231–236, 2002. https://doi.org/10.1016/S0167-6911(02)00119-6
• M. Harmouche, S. Laghrouche, Y. Chitour, M. Hamerlain, Stabilisation of perturbed chains of integrators using Lyapunov-based homogeneous controllers, Int. J. Control 90, 2631–2640, 2017. https://doi.org/10.1080/00207179.2016.1262967
• F. Lopez-Ramirez, D. Efimov, A. Polyakov, W. Perruquetti, Fixed-time output stabilization and fixed-time estimation of a chain of integrators, Int. J. Robust Nonlinear Control 28, 4647–4665, 2018. https://doi.org/10.1002/rnc.4275
• 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
• S. P. Bhat, D. S. Bernstein, Geometric homogeneity with applications to finite-time stability, Math. Control Signals Systems 17, 101–127, 2005. https://doi.org/10.1007/s00498-005-0151-x

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations makes a hybrid SDE mean-square exponentially stable when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval, and proved $H_\infty$-stability, asymptotic stability, and, in Section 4, exponential stability in mean square and almost surely with an explicit rate. This mission formalizes that exponential stability result, Theorem 4.2, and the steps of its proof.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$. The controlled system is

$$dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}$$

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

$$\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).$$

• Assumption 4.1: $c_1|x|^2\le U(x,i,t)\le c_2|x|^2$ with $c_1,c_2>0$.
• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

Put $\theta=K_3^2/\lambda_1$, $\lambda=\lambda_2-\theta\tau[2\tau(K_1^2+2K_3^2)+K_2^2]$ (positive by (3.5)), and

$$H_1=\theta\tau\big(2\tau(K_1^2+2K_3^2)+K_2^2\big)+\frac{24\theta\tau^4K_3^4}{1-6\tau^2K_3^2},\qquad H_2=\frac{12\theta\tau^2K_3^2(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}.$$

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Assumption41, Condition35, theta, lam, H1, H2, rateEquationLHS; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, solutions SolvesSampledHybridSDE, and the functional (4.7) Vbar, all in the namespace You2015.Expo.

Formalization targets

Goal: Theorem 4.2 (exponential stability)

Under the hypotheses above, the equation

$$2\tau\gamma e^{2\tau\gamma}(H_1+\tau H_2)+\gamma c_2=\lambda\tag{4.4}$$

has a unique root $\gamma>0$, and every solution of (2.1) satisfies

$$\limsup_{t\to\infty}\frac1t\log\big(\mathbb E|x(t)|^2\big)\le-\gamma,\qquad\limsup_{t\to\infty}\frac1t\log|x(t)|\le-\frac\gamma2\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$, $r_0\in S$.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (4.11) $\mathbb E\bar V(\hat x_z,\hat r_z,z)\le(H_1+\tau H_2)\int_{z-2\tau}^z\mathbb E|x(y)|^2dy$ for $z\ge2\tau$.
5. (4.14) $c_1e^{\gamma t}\mathbb E|x(t)|^2\le C$ for $t\ge2\tau$.
6. (4.14) $\Rightarrow$ (4.3), the mean-square-to-almost-sure transfer cited from Mao–Yuan [23, Theorem 8.8].

Significance

The result. Theorem 4.2 gives a quantitative guarantee: a controller that samples the state every $\tau$ units makes the switching system decay exponentially, with a rate $\gamma$ computable from the constants of the assumptions. Asymptotic stability (Section 3 of the paper) says nothing about how fast trajectories settle; the rate is what a designer trades against the sampling cost when choosing $\tau$. The almost sure statement concerns individual trajectories, which is what an operator observes.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1). Formalization also checks the constants: it found that the printed $H_1$ in (4.5) disagrees with the paper's own derivation (see below).

Difficulty

Equation (2.1) is a stochastic differential delay equation whose delay $t-\delta_t$ is bounded but jumps at every observation time, so the delay-equation stability theorems that require a differentiable delay with derivative below one (Mao–Yuan, p. 285) do not apply. A Lyapunov function of the current state alone leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval. An exponential rate requires controlling this delay term with an exponential weight, and the weight inflates the delay contribution by a factor $e^{2\tau\gamma}$; the rate equation (4.4) records exactly this balance. The almost sure part does not follow from the mean-square part by Chebyshev's inequality at fixed times alone: a pathwise bound needs control of the supremum of $|x|$ over each unit interval, which involves the martingale part of the solution.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5), (3.21), (4.5) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation of a nonnegative quantity ($\mathbb E|x|^2$, $\mathbb E\bar V$) and every time integral of one is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• Logarithms. The paper's $\log$ takes the value $-\infty$ at $0$. For a finite $a(t)\ge0$, $\limsup_{t\to\infty}\frac1t\log a(t)\le-\gamma$ is stated in the equivalent form "for every $\gamma'<\gamma$, eventually $a(t)\le e^{-\gamma't}$". Lean's Real.log 0 = 0 never enters. In (4.3) the almost-sure quantifier is outside the quantifier over $\gamma'$.
• Correction of (4.5). The page prints the last term of $H_1$ as $24\tau^3K_3^4/(1-6\tau^2K_3^2)$. Substituting (3.21) into (4.9), as the proof does, gives $24\theta\tau^4K_3^4/(1-6\tau^2K_3^2)$ (the same computation reproduces the printed $H_2$). The mission uses the corrected $H_1$ in the goal, (4.11) and (4.14). With the printed value the claimed rate could exceed what the proof yields whenever $\theta\tau>1$.
• "The unique root" is a conjunct of the goal ($\exists!\,\gamma>0$); the stability conclusions are stated for every positive root. "(so $\lambda>0$)" is a consequence of (3.5), not a hypothesis. (4.4) is kept as an equality.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,c_1,c_2,\tau$ are data. The constant $C$ of (4.14) is chosen after $x_0$, $r_0$, the solution and $\gamma$, and before $t$.
• (3.15), (3.21) and the transfer (4.14) $\Rightarrow$ (4.3) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. $\bar V$ of (4.7) is used only for $z\ge2\tau$, where no extension of the solution to negative times is needed. Other misprints on the page ($g(x,i,s)=f(x,i,0)$ on p. 909, $V(\hat x_0,\hat r_0,t)$ for $V(\hat x_0,\hat r_0,0)$ on p. 918, the swapped $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals, $\log 0$ is never evaluated, the goal asserts that the rate equation has exactly one positive root (so the stability clauses are not vacuous), the solution notion admits the true solution and requires path continuity, and the derivative witnesses of $U$ are tied to $U$. A sorry-free local check confirms that Assumptions 2.1, 2.2, 4.1, condition (3.5) and $\lambda>0$ hold for $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $K_1=K_2=K_3=1$, $\lambda_1=1/4$, $\lambda_2=1$, $c_1=c_2=1$, $\tau=1/10$; for these data $\mathcal LU+\lambda_1|U_x|^2=-|x|^2$ by hand.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, the Burkholder–Davis–Gundy inequality, and the Borel–Cantelli argument that turns mean-square exponential decay into almost sure decay. These are reusable far beyond this mission. Section 3 of the paper (asymptotic stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.1 for state feedback

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

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

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

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

Milestones

In attack order:

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations stabilizes a hybrid SDE in the sense of mean-square exponential stability when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval $\tau$, and proved $H_\infty$-stability, mean-square asymptotic stability, almost sure asymptotic stability and exponential stability of the controlled system. This mission formalizes the almost sure asymptotic stability result, Theorem 3.4, and the results it is built on.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$, the last observation time up to $t$. The controlled system is

$$dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}$$

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$. The feedback $u$ sees the state only at the observation times.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

$$\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).$$

• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Condition35, in the namespace You2015.Asymp; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, and solutions SolvesSampledHybridSDE, in the namespace You2015.Shared shared with the companion mission.

Formalization targets

Goal: Theorem 3.4 (almost sure asymptotic stability)

Under the hypotheses above, every solution of (2.1) satisfies

$$\lim_{t\to\infty}x(t)=0\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$ and $r_0\in S$. No rate is claimed; the statement is the qualitative convergence of almost every path.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (3.23) $\sup_{t\ge0}\mathbb E|x(t)|^2<\infty$.
5. $|\mathbb E|x(t_2)|^2-\mathbb E|x(t_1)|^2|\le C(t_2-t_1)$.
6. Theorem 3.3: $\lim_{t\to\infty}\mathbb E|x(t)|^2=0$.
7. (3.24)–(3.25): $\mathbb E\int_0^\infty|x(t)|^2dt<\infty$ and $\liminf_{t\to\infty}|x(t)|=0$ a.s.
8. (3.28): $\mathbb P(\exists t:|x(t)|\ge h)\le C/h^2$ for $h>|x_0|$.

Significance

The result. Theorem 3.4 says that a controller sampling the state at rate $1/\tau$ makes almost every trajectory of the switching system converge to the equilibrium, with an explicit, checkable bound (3.5) on $\tau$. Mean-square convergence (Theorem 3.3) does not imply almost sure convergence in general, and a single trajectory is what an operator observes, so the pathwise statement is the one relevant to a deployed system. Condition (3.5) is stated in terms of the constants of Assumptions 2.1, 2.2 and 3.1, so for a concrete system (Section 6 of the paper) it gives a numerical bound on the observation interval.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a reusable definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1).

Difficulty

Equation (2.1) is a stochastic differential delay equation with the delay $t-\delta_t$, which is bounded but jumps at every observation time and has derivative $1$ in between. The stability theorems for hybrid delay equations in the literature require a differentiable delay with derivative less than one (Mao–Yuan, p. 285), so they do not apply. Applying $\mathcal LU$ directly to $U(x(t),r(t),t)$ leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval, so a Lyapunov function of the current state alone does not close the argument.

For the goal, the natural first idea, deducing almost sure convergence from $\mathbb E|x(t)|^2\to0$ or from $\int_0^\infty|x(t)|^2dt<\infty$ a.s., fails: both are compatible with paths that make ever shorter excursions away from $0$. The obstacle is to exclude infinitely many excursions of a fixed size, which neither moment statement controls.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5) and (3.21) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation $\mathbb E|\cdot|^2$ and every time integral of a nonnegative quantity is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,\tau$ are data of each statement. The paper's "$C$ denotes a positive constant" is an existential chosen after $x_0$, $r_0$ and the solution, and before the time variables and $h$.
• (3.15) and (3.21) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. Misprints on the page (for example $g(x,i,s)=f(x,i,0)$ on p. 909 and the swapped definitions of $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals (which vanish for non-integrable integrands), the solution notion admits the true solution and requires path continuity, the derivative witnesses of $U$ are tied to $U$, and a sorry-free check shows that the data hypotheses (Assumptions 2.1, 2.2, 3.1, $C^{2,1}$, (3.5)) are satisfiable, for example by $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $\lambda_1=1/4$, $\lambda_2=1$, $\tau=1/10$.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, and Doob's maximal inequality in continuous time. These are reusable far beyond this mission. Section 4 of the paper (exponential stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005